SuperposedPotentialApproximation

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

Finite layer approximations of the superposed potential field

The full bad-component family need not be finite. This file truncates it by Whitney layer: the prefix at N contains every component active at a cube in a layer k < N. Such a prefix is finite, its slope defect is a zero-trace potential field, and on every earlier layer its cell value agrees exactly with the full superposed cell value.

The remaining cell defect has the same summable layer envelope, up to the harmless factor from vecNormSq_sub_le. The final L² closure argument is kept in a separate file.

Finite prefixes of the bad component family

theorem Algsuperdiff.Section3.Provider.Affine.whitneyScale_one_le {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ : ℕ) (omega : Cutoff.CutoffSample d) (hk₀ : 3 ≤ k₀) (j : ℕ) : 1 ≤ Whitney.whitneyScale M m E b k₀ omega j

The manuscript scale profile is at least one under its terminal lower bound 3 ≤ k₀.

noncomputable def Algsuperdiff.Section3.Provider.Affine.badFamilyComponentPrefix {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ : ℕ) (omega : Cutoff.CutoffSample d) (N : ℕ) : Finset (Set (HCPolySupport.TriadicCube d))

A finite prefix of the actual bad components. It contains the component of every bad cube in layers j ≤ N. The extra terminal layer is what makes the prefix contain all components active at cubes in layers k < N.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.badFamilyComponentPrefix_subset_badComponents {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ : ℕ) (omega : Cutoff.CutoffSample d) (N : ℕ) (C : Set (HCPolySupport.TriadicCube d)) : C ∈ badFamilyComponentPrefix M m E b k₀ omega N → C ∈ badComponents (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega)

theorem Algsuperdiff.Section3.Provider.Affine.activeComponent_mem_badFamilyComponentPrefix_of_lt {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hk₀ : 3 ≤ k₀) {N k : ℕ} (hk : k < N) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m E b k₀ omega) k) {C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ activeComponents m (Whitney.whitneyScale M m E b k₀ omega) (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) Q) : C ∈ badFamilyComponentPrefix M m E b k₀ omega N

Every component active at a cube in layer k < N occurs in the finite bad-family prefix.

theorem Algsuperdiff.Section3.Provider.Affine.potentialZeroTraceFieldOn_badFamily_activeComponentPrefix {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.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) => ∑ C ∈ badFamilyComponentPrefix M m E b k₀ omega N, (globalCompetitorSlope m (Whitney.simplexScale m (Whitney.whitneyScale M m E b k₀ omega) (componentWindowLayer m (Whitney.whitneyScale M m E b k₀ omega) C)) C p x - p)

Every finite active-layer prefix gives a zero-trace potential field.

Cell bounds for arbitrary finite partial sums

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_sum_globalCompetitorCellSlope_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) (A : Finset (Set (HCPolySupport.TriadicCube d))) (hA : ∀ C ∈ A, C ∈ badComponents (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega)) (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 (∑ C ∈ A, (globalCompetitorCellSlope m (Whitney.simplexScale m (Whitney.whitneyScale M m E b k₀ omega) (componentWindowLayer m (Whitney.whitneyScale M m E b k₀ omega) C)) C p T - p)) ≤ superposedGradConst d ^ 2 * 3 ^ (2 * (b * (↑k + ↑(Whitney.whitneyScale M m E b k₀ omega k)))) * HCPolySupport.vecNormSq p

Any finite partial sum of bad-component cell defects obeys the full superposed layer envelope. Components inactive at the current Whitney cube are removed before applying the multiplicity estimate.

Exactness and residual bounds

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitorCellSlope_sub_eq_activeComponentPrefix_sum {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 k : ℕ} (hk : 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) : superposedCompetitorCellSlope m (Whitney.whitneyScale M m E b k₀ omega) (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) p T - p = ∑ C ∈ badFamilyComponentPrefix M m E b k₀ omega N, (globalCompetitorCellSlope m (Whitney.simplexScale m (Whitney.whitneyScale M m E b k₀ omega) (componentWindowLayer m (Whitney.whitneyScale M m E b k₀ omega) C)) C p T - p)

On a cell in a layer below N, the full superposed cell defect is exactly the finite prefix sum.

The half-rate decay available under b ≤ 1/8

theorem Algsuperdiff.Section3.Provider.Affine.three_rpow_layerQuantity_half_decay {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hs k₀ k : ℕ) : 3 ^ (-↑k) * 3 ^ (2 * b * Multiscale.layerQuantity b hs k₀ k) ≤ 3 ^ (2 * b * (↑hs + ↑k₀ + 1)) * (3 ^ (-(1 / 2))) ^ k

The layer mass beats the squared collar growth at geometric rate 3^{-k/2} under the source window b ≤ 1/8. This deliberately uses a weaker rate than three_rpow_layerQuantity_decay, whose 4 α gate is unnecessary for the present L² closure argument.