PL1/EnfloTwoMaps.lean

All source files · Download exact source

SHA-256: 60e04362b9682583f3c3cfc2c954de402a4026f7e92d878cff60acb52abc3ba8

1import PL1.EnfloSum23/-!4# Two actual L1-valued maps cannot jointly be bounded below56Both maps have the same genuine interval L1 domain. Their two coordinates are7placed in the genuine ell1 sum, so the existing coordinatewise dyadic maximum8criterion applies without a direct-sum permanence assumption.9-/10noncomputable section11set_option backward.isDefEq.respectTransparency false12open MeasureTheory Filter13open scoped BigOperators Topology ENNReal14namespace PL1.EnfloBush15open IntervalModel1617section PairMap18variable {F Y : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]19  [NormedAddCommGroup Y] [NormedSpace ℝ Y]2021def pairMap (A B : F →L[ℝ] Y) : F →L[ℝ] L1Sum Y :=22  (lp.singleContinuousLinearMap ℝ (fun _ : ℕ => Y) 1 0).comp A +23    (lp.singleContinuousLinearMap ℝ (fun _ : ℕ => Y) 1 1).comp B2425@[simp] theorem pairMap_apply_zero (A B : F →L[ℝ] Y) (f : F) :26    pairMap A B f 0 = A f := by27  simp [pairMap]2829@[simp] theorem pairMap_apply_one (A B : F →L[ℝ] Y) (f : F) :30    pairMap A B f 1 = B f := by31  simp [pairMap]3233theorem pairMap_apply_other (A B : F →L[ℝ] Y) (f : F) (i : ℕ)34    (hi0 : i ≠ 0) (hi1 : i ≠ 1) : pairMap A B f i = 0 := by35  simp [pairMap, hi0, hi1]3637/-- The codomain norm is the sum of the two original norms. -/38theorem norm_pairMap (A B : F →L[ℝ] Y) (f : F) :39    ‖pairMap A B f‖ = ‖A f‖ + ‖B f‖ := by40  classical41  apply le_antisymm42  · change ‖(lp.single 1 (0 : ℕ) (A f) : L1Sum Y) + lp.single 1 (1 : ℕ) (B f)‖ ≤ _43    exact (norm_add_le _ _).trans_eq (by rw [lp.norm_single (by norm_num), lp.norm_single (by norm_num)])44  · have h := (L1Sum.summable_norm (pairMap A B f)).sum_le_tsum ({0,1} : Finset ℕ)45      (fun i _ => norm_nonneg _)46    simpa only [Finset.sum_insert (by simp : (0 : ℕ) ∉ ({1} : Finset ℕ)),47      Finset.sum_singleton, pairMap_apply_zero, pairMap_apply_one, ← L1Sum.norm_eq_tsum] using h48end PairMap4950variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)5152lemma dyadicVanishing_zero : DyadicVanishing (0 : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) := by53  have hz (m : ℕ) : dyadicMaxMass (0 : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) m = 0 :=54    le_antisymm (by simpa using dyadicMaxMass_le (0 : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) m)55      (dyadicMaxMass_nonneg _ _)56  change Tendsto (fun m => dyadicMaxMass (0 : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) m) atTop (𝓝 0)57  simp only [hz]58  exact tendsto_const_nhds5960/-- The real and imaginary parts of a hypothetical embedding may be tested61jointly, even when neither part alone is bounded below. -/62theorem not_boundedBelow_two_maps [SFinite μ]63    (A B : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ)64    (hA : DyadicVanishing A) (hB : DyadicVanishing B)65    {c : ℝ} (hc : 0 < c) (hlower : ∀ f, c*‖f‖ ≤ ‖A f‖ + ‖B f‖) : False := by66  apply not_boundedBelow_sum_of_coordinates μ (pairMap A B) ?_ hc67    (fun f => by rw [norm_pairMap]; exact hlower f)68  intro i69  by_cases hi0 : i = 070  · subst i71    have he : sumCoordinate μ (pairMap A B) 0 = A := by apply ContinuousLinearMap.ext; intro f; exact pairMap_apply_zero A B f72    rwa [he]73  by_cases hi1 : i = 174  · subst i75    have he : sumCoordinate μ (pairMap A B) 1 = B := by apply ContinuousLinearMap.ext; intro f; exact pairMap_apply_one A B f76    rwa [he]77  have he : sumCoordinate μ (pairMap A B) i = 0 := by78    apply ContinuousLinearMap.ext79    intro f80    exact pairMap_apply_other A B f i hi0 hi181  rw [he]82  exact dyadicVanishing_zero μ8384end PL1.EnfloBush8586