PL1/HeadTailNorms.lean

All source files · Download exact source

SHA-256: 510da205d5e54d48ea09800509fa56164c5f12e261a71aca987a74d6bd9f134f

1import PL1.HeadTail2import PL1.L1Multiplication34/-! # Actual Haar L1 norm preservation and spike separation -/56noncomputable section7open MeasureTheory8open scoped ENNReal9namespace PL1.HeadTail10open Walsh1112variable {K : Type*} [RCLike K]1314theorem norm_toLp (f : C(Walsh.Group, K)) :15    ‖ContinuousMap.toLp 1 haar K f‖ = ∫ x, ‖f x‖ ∂haar := by16  rw [L1.norm_eq_integral_norm]17  apply integral_congr_ae18  filter_upwards [ContinuousMap.coeFn_toLp (p := 1) (𝕜 := K) haar f] with x hx19  rw [hx]2021/-- Exact product norm; no positivity is required of the tail multiplier. -/22theorem norm_multiplier_toLp {S T : Finset ℕ} (hST : Disjoint S T)23    (f : C(Walsh.Group, K)) (q : C(Walsh.Group, ℝ))24    (hf : DependsOn S f) (hq : DependsOn T q) :25    ‖L1Multiplication.multiplier K q (ContinuousMap.toLp 1 haar K f)‖ =26      ‖ContinuousMap.toLp 1 haar ℝ q‖ * ‖ContinuousMap.toLp 1 haar K f‖ := by27  rw [L1Multiplication.multiplier_toLp, norm_toLp, norm_toLp, norm_toLp]28  exact integral_norm_smul hST f q hf hq2930/-- A nonnegative tail density of mass one preserves every finite head norm. -/31theorem norm_multiplier_toLp_of_density {S T : Finset ℕ} (hST : Disjoint S T)32    (f : C(Walsh.Group, K)) (q : C(Walsh.Group, ℝ))33    (hf : DependsOn S f) (hq : DependsOn T q)34    (hq0 : ∀ᵐ x ∂haar, 0 ≤ q x) (hq1 : ∫ x, q x ∂haar = 1) :35    ‖L1Multiplication.multiplier K q (ContinuousMap.toLp 1 haar K f)‖ =36      ‖ContinuousMap.toLp 1 haar K f‖ := by37  rw [norm_multiplier_toLp hST f q hf hq]38  have hn : ‖ContinuousMap.toLp 1 haar ℝ q‖ = 1 := by39    rw [norm_toLp, ← hq1]40    apply integral_congr_ae41    filter_upwards [hq0] with x hx42    exact Real.norm_of_nonneg hx43  rw [hn, one_mul]4445/-- Finite heads are separated by an actual concentrated tail multiplier on Haar L1. -/46theorem concentration_multiplier_toLp {S T : Finset ℕ} (hST : Disjoint S T)47    (f g : C(Walsh.Group, K)) (q : C(Walsh.Group, ℝ))48    (hf : DependsOn S f) (hg : DependsOn S g) (hq : DependsOn T q)49    (hq0 : ∀ᵐ x ∂haar, 0 ≤ q x) (hq1 : ∫ x, q x ∂haar = 1)50    (B : Set Walsh.Group) (hB : MeasurableSet B) (δ : ℝ)51    (hsmall : haar.real B ≤ δ) (hconcentrated : 1 - δ ≤ ∫ x in B, q x ∂haar) :52    (1 - 2 * δ) * (‖ContinuousMap.toLp 1 haar K f‖ + ‖ContinuousMap.toLp 1 haar K g‖) ≤53      ‖ContinuousMap.toLp 1 haar K f +54        L1Multiplication.multiplier K q (ContinuousMap.toLp 1 haar K g)‖ := by55  have hn : ‖ContinuousMap.toLp 1 haar K f +56      L1Multiplication.multiplier K q (ContinuousMap.toLp 1 haar K g)‖ =57        ∫ x, ‖f x + q x • g x‖ ∂haar := by58    rw [L1Multiplication.multiplier_toLp, ← map_add, norm_toLp]59    rfl60  rw [hn, norm_toLp, norm_toLp]61  exact concentration_lower_bound hST f g q hf hg hq hq0 hq1 B hB δ hsmall hconcentrated6263#print axioms norm_multiplier_toLp64#print axioms concentration_multiplier_toLp65end PL1.HeadTail66