On complemented subspaces of L1[0,1]L_1[0,1]

PL1/DisjointNormingFunctionals.lean

All source files · Download exact source

SHA-256: a9a0213ea4d8939c058110114a825aefd02618b1d0d114943cb319a8b713d47d

1import PL1.PrincipalIdealDual2import PL1.ComplementedLatticeBandEstimates3import PL1.SummingTransport4import Mathlib.Topology.Order.MonotoneConvergence56/-!7# Disjoint norming functionals without principal projections89Positive norming functionals are localized using scalar suprema of their10values on genuine lattice truncations. This removes the principal-projection11assumption from the finite summing-to-disjoint-norm estimate.12-/1314noncomputable section15open Filter16open scoped BigOperators Topology1718namespace PL1.DisjointNormingFunctionals19open PrincipalIdealDual PL1.ComplementedLattice2021variable {E : Type*} [NormedAddCommGroup E] [Lattice E]22  [IsOrderedAddMonoid E] [NormedVectorLattice E]2324private theorem orderDual_nonneg (ν : StrongDual ℝ E) (hν : 0 ≤ ν) :25    0 ≤ StrongDual.toOrderDualSpace ν := by26  apply OrderBoundedHom.le_iff.mpr27  intro x hx28  exact StrongDual.apply_nonneg_of_nonneg hν hx2930def localizationLinear (ν : StrongDual ℝ E) (hν : 0 ≤ ν) (a : E) (ha : 0 ≤ a) :31    E →ₗ[ℝ] ℝ :=32  (witOp (orderDual_nonneg ν hν) ha).toLinearMap3334theorem localizationLinear_positive (ν : StrongDual ℝ E) (hν : 0 ≤ ν)35    (a : E) (ha : 0 ≤ a) : Positive (localizationLinear ν hν a ha) :=36  witLin_positive (orderDual_nonneg ν hν) ha3738theorem localizationLinear_le (ν : StrongDual ℝ E) (hν : 0 ≤ ν)39    (a : E) (ha : 0 ≤ a) (x : E) (hx : 0 ≤ x) : localizationLinear ν hν a ha x ≤ ν x :=40  OrderBoundedHom.le_iff.mp (witOp_le_f (orderDual_nonneg ν hν) ha) x hx4142theorem localizationLinear_norm_le (ν : StrongDual ℝ E) (hν : 0 ≤ ν)43    (a : E) (ha : 0 ≤ a) (x : E) : ‖localizationLinear ν hν a ha x‖ ≤ ‖ν‖ * ‖x‖ := by44  calc45    _ = |localizationLinear ν hν a ha x| := Real.norm_eq_abs _46    _ ≤ localizationLinear ν hν a ha |x| :=47      Positive.abs_le_map_abs (localizationLinear_positive ν hν a ha) x48    _ ≤ ν |x| := localizationLinear_le ν hν a ha |x| (abs_nonneg x)49    _ ≤ |ν (|x|)| := le_abs_self _50    _ ≤ ‖ν‖ * ‖|x|‖ := ν.le_opNorm _51    _ = _ := by rw [norm_abs_eq_norm]5253/-- A positive contractive localization of a continuous functional. -/54def localization (ν : StrongDual ℝ E) (hν : 0 ≤ ν) (a : E) (ha : 0 ≤ a) :55    StrongDual ℝ E :=56  (localizationLinear ν hν a ha).mkContinuous ‖ν‖57    (localizationLinear_norm_le ν hν a ha)5859theorem localization_nonneg (ν : StrongDual ℝ E) (hν : 0 ≤ ν) (a : E) (ha : 0 ≤ a) :60    0 ≤ localization ν hν a ha :=61  StrongDual.nonneg_iff.mpr (localizationLinear_positive ν hν a ha)6263theorem norm_localization_le (ν : StrongDual ℝ E) (hν : 0 ≤ ν) (a : E) (ha : 0 ≤ a) :64    ‖localization ν hν a ha‖ ≤ ‖ν‖ :=65  (localizationLinear ν hν a ha).mkContinuous_norm_le (norm_nonneg ν)66    (localizationLinear_norm_le ν hν a ha)6768theorem localization_self (ν : StrongDual ℝ E) (hν : 0 ≤ ν) (a : E) (ha : 0 ≤ a) :69    localization ν hν a ha a = ν a :=70  witOp_apply_self (orderDual_nonneg ν hν) ha7172theorem localization_isLUB (ν : StrongDual ℝ E) (hν : 0 ≤ ν) (a : E) (ha : 0 ≤ a)73    (x : E) (hx : 0 ≤ x) :74    IsLUB (Set.range fun n : ℕ => ν (x ⊓ n • a)) (localization ν hν a ha x) := by75  change IsLUB _ (witLin (orderDual_nonneg ν hν) ha x)76  rw [witLin_apply_nonneg (orderDual_nonneg ν hν) ha hx]77  exact witFun_isLUB (orderDual_nonneg ν hν) ha hx7879theorem tendsto_truncation_localization (ν : StrongDual ℝ E) (hν : 0 ≤ ν)80    (a : E) (ha : 0 ≤ a) (x : E) (hx : 0 ≤ x) :81    Tendsto (fun n : ℕ => ν (x ⊓ n • a)) atTop (𝓝 (localization ν hν a ha x)) := by82  apply tendsto_atTop_isLUB _ (localization_isLUB ν hν a ha x hx)83  intro n m hnm84  apply StrongDual.apply_le_apply_of_nonneg hν85  exact inf_le_inf_left _ (nsmul_le_nsmul_left ha hnm)868788/-- Genuine finite truncations inherit disjointness from their generators. -/89theorem truncations_disjoint (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)90    (hd : Pairwise fun i j => IsVLDisjoint (a i) (a j)) (x : E) (n : ℕ) :91    Pairwise fun i j => IsVLDisjoint (|x| ⊓ n • a i) (|x| ⊓ n • a j) := by92  intro i j hij93  have hbase : IsVLDisjoint (n • a i) (n • a j) := by94    simpa only [Nat.cast_smul_eq_nsmul] using95      ((hd hij).smul_left (n : ℝ)).smul_right (n : ℝ)96  apply (hbase.mono_left ?_).mono_right ?_97  · rw [abs_of_nonneg (le_inf (abs_nonneg x) (nsmul_nonneg (ha i) n)),98      abs_of_nonneg (nsmul_nonneg (ha i) n)]99    exact inf_le_right100  · rw [abs_of_nonneg (le_inf (abs_nonneg x) (nsmul_nonneg (ha j) n)),101      abs_of_nonneg (nsmul_nonneg (ha j) n)]102    exact inf_le_right103104theorem norm_sum_truncations_le (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)105    (hd : Pairwise fun i j => IsVLDisjoint (a i) (a j)) (x : E) (n : ℕ) :106    ‖∑ i, |x| ⊓ n • a i‖ ≤ ‖x‖ := by107  apply norm_le_norm_of_abs_le_abs108  apply abs_disjoint_sum_le d _ (truncations_disjoint d a ha hd x n) x109  intro i110  rw [abs_of_nonneg (le_inf (abs_nonneg x) (nsmul_nonneg (ha i) n))]111  exact inf_le_left112113/-- The actual two-summing hypothesis controls every finite truncation level. -/114theorem truncation_square_sum_le (C : ℝ) (hC : 0 ≤ C)115    (hTwo : ∀ (d : ℕ) (T : (Fin d → ℝ) →L[ℝ] E), TwoSummingWith T (C * ‖T‖))116    (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)117    (hd : Pairwise fun i j => IsVLDisjoint (a i) (a j))118    (ν : Fin d → StrongDual ℝ E) (hνnorm : ∀ i, ‖ν i‖ ≤ 1) (x : E) (n : ℕ) :119    ∑ i, (ν i (|x| ⊓ n • a i)) ^ 2 ≤ C ^ 2 * ‖x‖ ^ 2 := by120  let y : Fin d → E := fun i => |x| ⊓ n • a i121  have hy := truncations_disjoint d a ha hd x n122  let T := disjointSynthesis d y hy123  have hTnorm : ‖T‖ ≤ ‖x‖ :=124    (norm_disjointSynthesis_le d y hy).trans (norm_sum_truncations_le d a ha hd x n)125  calc126    _ ≤ ∑ i, ‖y i‖ ^ 2 := by127      apply Finset.sum_le_sum128      intro i _129      simpa only [Real.norm_eq_abs, sq_abs, one_mul] using130        pow_le_pow_left₀ (norm_nonneg _) ((ν i).le_of_opNorm_le (hνnorm i) (y i)) 2131    _ ≤ (C * ‖T‖) ^ 2 := disjoint_square_sum_le_of_twoSumming d y hy (hTwo d T)132    _ ≤ (C * ‖x‖) ^ 2 :=133      pow_le_pow_left₀ (mul_nonneg hC (norm_nonneg T))134        (mul_le_mul_of_nonneg_left hTnorm hC) 2135    _ = _ := mul_pow _ _ 2136137/-- Scalar monotone convergence supplies the localized square estimate;138no primal vector-lattice supremum or weak completeness is invoked. -/139theorem localization_square_sum_le (C : ℝ) (hC : 0 ≤ C)140    (hTwo : ∀ (d : ℕ) (T : (Fin d → ℝ) →L[ℝ] E), TwoSummingWith T (C * ‖T‖))141    (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)142    (hd : Pairwise fun i j => IsVLDisjoint (a i) (a j))143    (ν : Fin d → StrongDual ℝ E) (hν : ∀ i, 0 ≤ ν i) (hνnorm : ∀ i, ‖ν i‖ ≤ 1)144    (x : E) :145    ∑ i, (localization (ν i) (hν i) (a i) (ha i) x) ^ 2 ≤ C ^ 2 * ‖x‖ ^ 2 := by146  have ht : Tendsto (fun n : ℕ => ∑ i, (ν i (|x| ⊓ n • a i)) ^ 2) atTop147      (𝓝 (∑ i, (localization (ν i) (hν i) (a i) (ha i) |x|) ^ 2)) := by148    apply tendsto_finsetSum149    intro i _150    exact (tendsto_truncation_localization (ν i) (hν i) (a i) (ha i) |x| (abs_nonneg x)).pow 2151  have hlim := le_of_tendsto ht (Eventually.of_forall152    (truncation_square_sum_le C hC hTwo d a ha hd ν hνnorm x))153  apply le_trans _ hlim154  apply Finset.sum_le_sum155  intro i _156  simpa only [sq_abs] using pow_le_pow_left₀ (abs_nonneg _)157    (StrongDual.abs_apply_le_apply_abs (localization_nonneg (ν i) (hν i) (a i) (ha i)) x) 2158159def coordinates (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)160    (ν : Fin d → StrongDual ℝ E) (hν : ∀ i, 0 ≤ ν i) :161    E →L[ℝ] EuclideanSpace ℝ (Fin d) :=162  (EuclideanSpace.equiv (Fin d) ℝ).symm.toContinuousLinearMap.comp163    (ContinuousLinearMap.pi fun i => localization (ν i) (hν i) (a i) (ha i))164165@[simp] theorem coordinates_apply (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)166    (ν : Fin d → StrongDual ℝ E) (hν : ∀ i, 0 ≤ ν i) (x : E) (i : Fin d) :167    coordinates d a ha ν hν x i = localization (ν i) (hν i) (a i) (ha i) x := rfl168169theorem norm_coordinates_le (C : ℝ) (hC : 0 ≤ C)170    (hTwo : ∀ (d : ℕ) (T : (Fin d → ℝ) →L[ℝ] E), TwoSummingWith T (C * ‖T‖))171    (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)172    (hd : Pairwise fun i j => IsVLDisjoint (a i) (a j))173    (ν : Fin d → StrongDual ℝ E) (hν : ∀ i, 0 ≤ ν i) (hνnorm : ∀ i, ‖ν i‖ ≤ 1) :174    ‖coordinates d a ha ν hν‖ ≤ C := by175  apply ContinuousLinearMap.opNorm_le_bound _ hC176  intro x177  apply (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hC (norm_nonneg x))).mp178  rw [EuclideanSpace.real_norm_sq_eq, mul_pow]179  exact localization_square_sum_le C hC hTwo d a ha hd ν hν hνnorm x180181/-- The finite disjoint lower-1 estimate holds without principal projections. -/182theorem positive_disjoint_sum_norm_le (C : ℝ) (hC : 0 ≤ C)183    (hOne : ∀ (d : ℕ) (S : E →L[ℝ] EuclideanSpace ℝ (Fin d)), OneSummingWith S (C * ‖S‖))184    (hTwo : ∀ (d : ℕ) (T : (Fin d → ℝ) →L[ℝ] E), TwoSummingWith T (C * ‖T‖))185    (d : ℕ) (a : Fin d → E) (ha : ∀ i, 0 ≤ a i)186    (hd : Pairwise fun i j => IsVLDisjoint (a i) (a j)) :187    ∑ i, ‖a i‖ ≤ C ^ 2 * ‖∑ i, a i‖ := by188  choose ν hν hνnorm hνa using fun i => StrongDual.exists_positive_dual_norming (ha i)189  let S := coordinates d a ha ν hν190  have hSnorm : ‖S‖ ≤ C := norm_coordinates_le C hC hTwo d a ha hd ν hν hνnorm191  have hdiag (i : Fin d) : ‖a i‖ ≤ ‖S (a i)‖ := by192    have hentry : S (a i) i = ‖a i‖ := by193      change localization (ν i) (hν i) (a i) (ha i) (a i) = _194      rw [localization_self, hνa i]195    have h := PiLp.norm_apply_le (S (a i)) i196    simpa only [hentry, Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)] using h197  calc198    _ ≤ ∑ i, ‖S (a i)‖ := Finset.sum_le_sum (fun i _ => hdiag i)199    _ ≤ (C * ‖S‖) * ‖∑ i, a i‖ := (hOne d S).disjoint_sum_le d a hd200    _ ≤ C ^ 2 * ‖∑ i, a i‖ := by201      rw [pow_two]202      exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hSnorm hC) (norm_nonneg _)203204theorem disjoint_sum_norm_le (C : ℝ) (hC : 0 ≤ C)205    (hOne : ∀ (d : ℕ) (S : E →L[ℝ] EuclideanSpace ℝ (Fin d)), OneSummingWith S (C * ‖S‖))206    (hTwo : ∀ (d : ℕ) (T : (Fin d → ℝ) →L[ℝ] E), TwoSummingWith T (C * ‖T‖))207    (d : ℕ) (x : Fin d → E) (hd : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :208    ∑ i, ‖x i‖ ≤ C ^ 2 * ‖∑ i, x i‖ := by209  have habs : Pairwise fun i j => IsVLDisjoint |x i| |x j| := by210    intro i j hij211    simpa only [IsVLDisjoint, abs_abs] using hd hij212  have h := positive_disjoint_sum_norm_le C hC hOne hTwo d (fun i => |x i|)213    (fun i => abs_nonneg _) habs214  have hsum : |∑ i, x i| = ∑ i, |x i| := by215    simpa only [one_smul, abs_one] using216      (abs_sum_of_pairwise_isVLDisjoint (α := fun _ => (1 : ℝ)) hd)217  rw [← hsum, norm_abs_eq_norm] at h218  simpa only [norm_abs_eq_norm] using h219220221/-- The summing-to-lattice consequence for an actual complemented copy,222with no principal-projection hypothesis on the lattice. -/223theorem disjoint_sum_norm_le_of_complemented_ambient224    {Y : Type*} [NormedAddCommGroup Y] [NormedSpace ℝ Y]225    (Q : EnfloStarbird.ComplementedCopy ℝ E Y) {G : ℝ} (hG : 0 ≤ G)226    (hOne : ∀ (n : ℕ) (S : Y →L[ℝ] EuclideanSpace ℝ (Fin n)), OneSummingWith S (G * ‖S‖))227    (hTwo : ∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] Y), TwoSummingWith T (G * ‖T‖))228    (d : ℕ) (x : Fin d → E) (hd : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :229    ∑ i, ‖x i‖ ≤ (G * ‖Q.embedding‖ * ‖Q.retraction‖) ^ 2 * ‖∑ i, x i‖ := by230  obtain ⟨hC, hOneE, hTwoE⟩ := uniform_finite_summing_estimates Q hG hOne hTwo231  exact disjoint_sum_norm_le _ hC hOneE hTwoE d x hd232233end PL1.DisjointNormingFunctionals234