PL1/LatticeRademacher.lean
All source files · Download exact source
SHA-256: 905ffd7701009006eb73129eefd20cb7038528ab4eb9147e6590efe3093ac0c5
1import PL1.LatticeAbsoluteContinuity2import Mathlib.Algebra.Order.BigOperators.Ring.Finset34/-!5# Finite orthogonal fragment estimates67This module supplies the analytic part of the atomless-lattice Rademacher8argument. Fragment partitions and their scalar orthogonality are explicit9inputs; their existence is not assumed as a lattice instance.10-/1112noncomputable section13open Filter TopologicalSpace Finset14open scoped Topology1516namespace PL1.SchurLattice1718variable {E : Type*} [NormedAddCommGroup E] [Lattice E]19 [IsOrderedAddMonoid E] [NormedVectorLattice E]2021/-- The finite disjoint modulus identity with an arbitrary finite index22type; this extends BanLat's `Fin n` formulation. -/23theorem abs_sum_smul_disjoint {ι : Type*} [Fintype ι] (p : ι → E) (a : ι → ℝ)24 (hd : Pairwise (fun i j => IsVLDisjoint (p i) (p j))) :25 |∑ i, a i • p i| = ∑ i, |a i| • |p i| := by26 classical27 let e := (Fintype.equivFin ι).symm28 have h := abs_sum_of_pairwise_isVLDisjoint (x := fun i => p (e i))29 (α := fun i => a (e i)) (fun i j hij => hd (e.injective.ne hij))30 rw [e.sum_comp (fun i => a i • p i), e.sum_comp (fun i => |a i| • |p i|)] at h31 exact h3233/-- Weighted finite Cauchy--Schwarz in the lattice modulus seminorm. -/34theorem dual_abs_sum_sq_le {ι : Type*} [Fintype ι]35 (φ : E →L[ℝ] ℝ) (hφ : 0 ≤ φ) (p : ι → E) (a : ι → ℝ)36 (hp : ∀ i, 0 ≤ p i) (hd : Pairwise (fun i j => IsVLDisjoint (p i) (p j))) :37 (φ |∑ i, a i • p i|) ^ 2 ≤ φ (∑ i, p i) * ∑ i, (a i) ^ 2 * φ (p i) := by38 classical39 rw [abs_sum_smul_disjoint p a hd]40 simp_rw [abs_of_nonneg (hp _), map_sum, map_smul, smul_eq_mul]41 apply sum_sq_le_sum_mul_sum_of_sq_le_mul univ42 (f := fun i => φ (p i)) (g := fun i => a i ^ 2 * φ (p i))43 · intro i _44 exact StrongDual.apply_nonneg_of_nonneg hφ (hp i)45 · intro i _46 exact mul_nonneg (sq_nonneg _) (StrongDual.apply_nonneg_of_nonneg hφ (hp i))47 · intro i _48 rw [mul_pow, sq_abs]49 exact le_of_eq (by ring)5051/-- Expanding a finite weighted orthogonal system gives the exact square52sum, without any infinite-dimensional spectral theorem. -/53theorem sum_sq_eq_of_weighted_orthogonal {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι]54 (σ : ι → κ → ℝ) (w : κ → ℝ) (W : ℝ)55 (hσ : ∀ i k, (∑ j, w j * σ i j * σ k j) = if i = k then W else 0)56 (a : ι → ℝ) :57 (∑ j, (∑ i, a i * σ i j) ^ 2 * w j) = W * ∑ i, a i ^ 2 := by58 classical59 have hexpand (j : κ) : (∑ i, a i * σ i j) ^ 2 * w j =60 ∑ i, ∑ k, a i * a k * (w j * σ i j * σ k j) := by61 rw [pow_two, sum_mul, sum_mul]62 apply sum_congr rfl63 intro i _64 rw [mul_sum, sum_mul]65 apply sum_congr rfl66 intro k _67 ring68 simp_rw [hexpand]69 rw [sum_comm]70 simp_rw [sum_comm (f := fun j k => a _ * a k * (w j * σ _ j * σ k j))]71 simp_rw [← mul_sum, hσ]72 simp only [mul_ite, mul_zero]73 rw [mul_sum]74 apply sum_congr rfl75 intro i _76 simp [mul_comm, pow_two]7778/-- Orthogonal signs on a positive disjoint partition give an actual79lattice estimate for all finite scalar combinations. -/80theorem dual_abs_sum_sq_le_of_orthogonal_fragments81 {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι]82 (φ : E →L[ℝ] ℝ) (hφ : 0 ≤ φ) (u : E)83 (p : κ → E) (hp : ∀ j, 0 ≤ p j)84 (hd : Pairwise (fun i j => IsVLDisjoint (p i) (p j)))85 (hsum : ∑ j, p j = u) (r : ι → E) (σ : ι → κ → ℝ)86 (hr : ∀ i, r i = ∑ j, σ i j • p j)87 (hσ : ∀ i k, (∑ j, φ (p j) * σ i j * σ k j) =88 if i = k then φ u else 0) (a : ι → ℝ) :89 (φ |∑ i, a i • r i|) ^ 2 ≤ (φ u) ^ 2 * ∑ i, a i ^ 2 := by90 classical91 have heq : (∑ i, a i • r i) = ∑ j, (∑ i, a i * σ i j) • p j := by92 simp_rw [hr, smul_sum, smul_smul, sum_smul]93 exact sum_comm94 rw [heq]95 have h := dual_abs_sum_sq_le φ hφ p (fun j => ∑ i, a i * σ i j) hp hd96 rw [hsum, sum_sq_eq_of_weighted_orthogonal σ (fun j => φ (p j)) (φ u) hσ a] at h97 convert h using 1; ring9899end PL1.SchurLattice100