SuperposedPotentialL2

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The full superposed slope defect is a zero-trace potential field

Finite Whitney-layer prefixes of the bad-component superposition are genuine zero-trace potential fields. This file proves that those prefixes are Cauchy in L², identifies their limit almost everywhere with the full superposed slope defect, and uses the closed-range realization on the open root cube.

The L² argument is non-circular: every integral used in the Cauchy estimate is an integral of a difference of two finite prefixes, whose MemVectorL2 witnesses are already supplied by the finite potential theorem.

The finite fields and their cell constants

noncomputable def Algsuperdiff.Section3.Provider.Affine.badFamilyPotentialApproximation {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ : ℕ) (omega : Cutoff.CutoffSample d) (N : ℕ) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The finite bad-component slope defect obtained by truncating in Whitney layer.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Affine.badFamilyPotentialApproximationCell {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ : ℕ) (omega : Cutoff.CutoffSample d) (N : ℕ) (p : HCPolySupport.Vec d) (T : Whitney.KuhnCell d) : HCPolySupport.Vec d

The cell constant associated with a finite bad-component prefix.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Affine.badFamilyPotentialApproximation_eq_cell {d : ℕ} [NeZero d] {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ N : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.simplexPartition m (Whitney.whitneyScale M m E b k₀ omega)) (x : HCPolySupport.Vec d) : x ∈ T.openCarrier → badFamilyPotentialApproximation M m E b k₀ omega N p x = badFamilyPotentialApproximationCell M m E b k₀ omega N p T

A finite prefix is constant on every open simplex cell, with the advertised finite cell sum as its value.

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_badFamilyPotentialApproximationCell_sub_le_layerEnvelope {d : ℕ} [NeZero d] {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (N N' : ℕ) (p : HCPolySupport.Vec d) {k : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m E b k₀ omega) k) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m (Whitney.whitneyScale M m E b k₀ omega) k Q) : HCPolySupport.vecNormSq (badFamilyPotentialApproximationCell M m E b k₀ omega N p T - badFamilyPotentialApproximationCell M m E b k₀ omega N' p T) ≤ (2 * superposedGradConst d) ^ 2 * 3 ^ (2 * (b * (↑k + ↑(Whitney.whitneyScale M m E b k₀ omega k)))) * HCPolySupport.vecNormSq p

The difference of two finite prefixes obeys the same layer envelope, up to the elementary factor from vecNormSq_sub_le.

theorem Algsuperdiff.Section3.Provider.Affine.badFamilyPotentialApproximationCell_eq_of_layer_lt {d : ℕ} [NeZero d] {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) {N N' k : ℕ} (hkN : k < N) (hkN' : k < N') (p : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m E b k₀ omega) k) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m (Whitney.whitneyScale M m E b k₀ omega) k Q) : badFamilyPotentialApproximationCell M m E b k₀ omega N p T = badFamilyPotentialApproximationCell M m E b k₀ omega N' p T

Below the smaller cutoff, two finite prefixes have identical cell value.

The L² increment estimate

noncomputable def Algsuperdiff.Section3.Provider.Affine.badFamilyPotentialApproximationL2 {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (N : ℕ) (p : HCPolySupport.Vec d) : ↥(HCPolySupport.VectorL2 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))

The canonical VectorL2 class of a finite prefix.

Equations

• Algsuperdiff.Section3.Provider.Affine.badFamilyPotentialApproximationL2 hb0 hb hk₀ hne N p = HCPolySupport.toVectorL2 ⋯

theorem Algsuperdiff.Section3.Provider.Affine.integral_vecNormSq_badFamilyPotentialApproximation_sub_succ_le {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (N : ℕ) (p : HCPolySupport.Vec d) : ∫ (x : HCPolySupport.Vec d) in HCPolySupport.openCubeSet (HCPolySupport.originCube d m), HCPolySupport.vecNormSq (badFamilyPotentialApproximation M m E b k₀ omega N p x - badFamilyPotentialApproximation M m E b k₀ omega (N + 1) p x) ≤ HCPolySupport.cubeVolume (HCPolySupport.originCube d m) * (6 * ↑d * (2 * superposedGradConst d) ^ 2 * HCPolySupport.vecNormSq p * 3 ^ (2 * b * (↑(Percolation.hsep M m E b omega) + ↑k₀ + 1))) * (3 ^ (-(1 / 2))) ^ N * (1 - 3 ^ (-(1 / 2)))⁻¹

The squared finite-prefix increment, integrated over the root cube, has a geometrically decaying upper bound.

noncomputable def Algsuperdiff.Section3.Provider.Affine.badFamilyPotentialIncrementConst {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ : ℕ) (omega : Cutoff.CutoffSample d) (p : HCPolySupport.Vec d) : ℝ

The explicit L² budget for potential increments over a bad family.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Affine.dist_badFamilyPotentialApproximationL2_succ_le {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (N : ℕ) (p : HCPolySupport.Vec d) : dist (badFamilyPotentialApproximationL2 hb0 hb hk₀ hne N p) (badFamilyPotentialApproximationL2 hb0 hb hk₀ hne (N + 1) p) ≤ √(badFamilyPotentialIncrementConst M m E b k₀ omega p) * (3 ^ (-(1 / 4))) ^ N

Consecutive finite-prefix classes have a summable geometric distance majorant.

theorem Algsuperdiff.Section3.Provider.Affine.cauchySeq_badFamilyPotentialApproximationL2 {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (p : HCPolySupport.Vec d) : CauchySeq fun (N : ℕ) => badFamilyPotentialApproximationL2 hb0 hb hk₀ hne N p

The finite bad-family potential approximations form a Cauchy sequence in the canonical vector L² space.