PL1/EnfloSum.lean

All source files · Download exact source

SHA-256: 02eb1e868392e6ee6e28fe4b9d4bbe9d803133b988d5c82d003c0b2367453811

1import PL1.EnfloMajorant2import PL1.DyadicCoordinateDomination3import PL1.IntervalModel45/-! Coordinatewise dyadic maximum decay excludes an L1 copy in a true ell1 sum. -/67noncomputable section8set_option backward.isDefEq.respectTransparency false9open MeasureTheory Filter10open scoped BigOperators Topology ENNReal1112namespace PL1.EnfloBush13open IntervalModel DyadicTrace1415variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [SFinite μ]1617theorem maxMass_flatten (n : ℕ) (f : ℕ → L1Sum (Lp ℝ 1 μ)) :18    maxMass n (fun j => flatten μ (f j)) =19      ∑' i, maxMass n (fun j => f j i) := by20  have he : (fun z => maxAbs n (fun j => flatten μ (f j) z)) =ᵐ[disjointMeasure μ]21      (fun z : ℕ × Ω => maxAbs n (fun j => f j z.1 z.2)) := by22    filter_upwards [ae_all_iff.mpr (fun j => flatten_coeFn μ (f j))] with z hz23    exact maxAbs_congr (fun j _ => hz j)24  have hi : Integrable (fun z : ℕ × Ω => maxAbs n (fun j => f j z.1 z.2))25      (Measure.count.prod μ) := (integrable_maxAbs n (fun j => flatten μ (f j))).congr he26  rw [maxMass, integral_congr_ae he, disjointMeasure, integral_prod _ hi,27    integral_countable hi.integral_prod_left]28  simp [measureReal_def, maxMass]2930def sumCoordinate (T : IntervalL1 ℝ →L[ℝ] L1Sum (Lp ℝ 1 μ)) (i : ℕ) :31    IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ :=32  (lp.evalCLM ℝ (fun _ : ℕ => Lp ℝ 1 μ) 1 i).comp T3334omit [SFinite μ] in35theorem sumCoordinate_apply (T : IntervalL1 ℝ →L[ℝ] L1Sum (Lp ℝ 1 μ))36    (i : ℕ) (f : IntervalL1 ℝ) : sumCoordinate μ T i f = T f i := rfl3738omit [SFinite μ] in39theorem sum_dyadicSumMass_le (T : IntervalL1 ℝ →L[ℝ] L1Sum (Lp ℝ 1 μ))40    (m : ℕ) (s : Finset ℕ) : ∑ i ∈ s, dyadicSumMass (sumCoordinate μ T i) m ≤ ‖T‖ := by41  classical42  simp only [dyadicSumMass, sumCoordinate_apply]43  rw [Finset.sum_comm]44  calc45    _ ≤ ∑ j ∈ Finset.range (2 ^ m), ‖T (dyadicVector (𝕜 := ℝ) m j)‖ := by46      apply Finset.sum_le_sum47      intro j hj48      rw [L1Sum.norm_eq_tsum]49      exact (L1Sum.summable_norm (T (dyadicVector m j))).sum_le_tsum s50        (fun i hi => norm_nonneg _)51    _ ≤ ∑ j ∈ Finset.range (2 ^ m), ‖T‖ * ‖dyadicVector (𝕜 := ℝ) m j‖ :=52      Finset.sum_le_sum (fun j _ => T.le_opNorm _)53    _ = ‖T‖ := by rw [← Finset.mul_sum, EnfloBush.sum_norm_dyadicVector, mul_one]5455theorem dyadicMaxMass_flatten (T : IntervalL1 ℝ →L[ℝ] L1Sum (Lp ℝ 1 μ)) (m : ℕ) :56    dyadicMaxMass ((flattenIsometry (𝕜 := ℝ) μ).toContinuousLinearMap.comp T) m =57      ∑' i, dyadicMaxMass (sumCoordinate μ T i) m :=58  maxMass_flatten μ (2 ^ m) (fun j => T (dyadicVector m j))5960theorem dyadicVanishing_flatten_of_coordinates61    (T : IntervalL1 ℝ →L[ℝ] L1Sum (Lp ℝ 1 μ))62    (h : ∀ i, DyadicVanishing (sumCoordinate μ T i)) :63    DyadicVanishing ((flattenIsometry (𝕜 := ℝ) μ).toContinuousLinearMap.comp T) := by64  change Tendsto (fun m => dyadicMaxMass65    ((flattenIsometry (𝕜 := ℝ) μ).toContinuousLinearMap.comp T) m) atTop (𝓝 0)66  simp_rw [dyadicMaxMass_flatten]67  apply DyadicCoordinateDomination.tendsto_tsum_zero_of_increasing_majorants68    (fun m i => dyadicSumMass (sumCoordinate μ T i) m) _ ‖T‖69  · intro m i70    exact dyadicSumMass_nonneg _ _71  · intro i72    exact dyadicSumMass_monotone _73  · exact sum_dyadicSumMass_le μ T74  · intro m i75    exact dyadicMaxMass_nonneg _ _76  · intro m i77    exact dyadicMaxMass_le_sum _ _78  · exact h7980theorem not_boundedBelow_sum_of_coordinates81    (T : IntervalL1 ℝ →L[ℝ] L1Sum (Lp ℝ 1 μ))82    (h : ∀ i, DyadicVanishing (sumCoordinate μ T i))83    {c : ℝ} (hc : 0 < c) (hlower : ∀ f, c * ‖f‖ ≤ ‖T f‖) : False := by84  apply not_boundedBelow_of_dyadicVanishing85    (dyadicVanishing_flatten_of_coordinates μ T h) hc86  intro f87  simpa only [ContinuousLinearMap.comp_apply, LinearIsometry.coe_toContinuousLinearMap,88    LinearIsometry.norm_map] using hlower f8990end PL1.EnfloBush91