SharpFramedMeanLayers

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

Framed potential-only Whitney-layer bounds

The observation-to-cube scale frame from the normalized potential response is constant across a fixed Whitney layer. This file keeps that frame outside the fourth-mass square root when the cellwise estimates are aggregated.

These are internal conditional proof obligations.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeMeanLayerFrame {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (i : ℤ) : ℝ

The observation-to-cube frame on the nth Whitney layer.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.probeMeanLayerFrame M m hn n i = 3 ^ (-(M.gamma * ↑(i - (m - ↑n - ↑(hn n)))))

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeFramedLayerWaveFactor {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) : ℝ

The simplex fourth-mass wave factor with the layer frame retained outside the square root.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeFramedGoodLayerMeanRhs {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) (p : HCPolySupport.Vec d) : ℝ

The good Whitney-layer mean budget combining its mass and wave contributions.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeFramedCollarLayerMeanRhs {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) (p : HCPolySupport.Vec d) (Cgrad b : ℝ) : ℝ

The collar-layer mean budget including the amplified gradient factor.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probeMeanLayerFrame_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (i : ℤ) : 0 ≤ probeMeanLayerFrame M m hn n i

theorem Algsuperdiff.Section3.Provider.Multiscale.probeFramedLayerWaveFactor_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeFramedLayerWaveFactor M m hn n i L omega

theorem Algsuperdiff.Section3.Provider.Multiscale.probeFramedMeanCellMajorant_potential_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (k i L : ℤ) (omega : Cutoff.CutoffSample d) (T : Whitney.KuhnCell d) (p : HCPolySupport.Vec d) (hW : HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k (1 / 4) ≤ 3) : probeFramedMeanCellMajorant M Q k i L omega T p 0 ≤ probeMeanGoodBaseConst d * HCPolySupport.vecNormSq p + probeMeanGoodWaveConst M * 3 ^ (-(M.gamma * ↑(i - Q.scale))) * M.gamma * 3 ^ (-(2 * M.gamma * ↑Q.scale)) * HCPolySupport.Book.Ch02.matrixOperatorNorm (simplexIncrementValue Q.scale L (↑omega) T) ^ 2 * HCPolySupport.vecNormSq p

Potential specialization of the framed cell majorant after the geometric descendant weight is bounded by three.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_sum_ofReal_goodCellForm_layer_le_framedMeanFourth_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (hstep : hn n ≤ hn (n + 1) + 1) (hgap : hn (n + 1) ≤ hn n + 1) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m0) {L : ℤ} (hmL : m ≤ L) (p : HCPolySupport.Vec d) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∑ Q ∈ Whitney.whitneyLayer m hn n, ∑ T ∈ Whitney.whitneySimplexCells m hn n Q, ENNReal.ofReal (cellWeight m T * goodCellForm M m hn L omega ((√↑(Annealed.sigmaBar M i))⁻¹ • p) 0 T) ≤ ENNReal.ofReal (probeFramedGoodLayerMeanRhs M m hn n i L omega p)

Internal conditional aggregation of the framed potential majorant over a good Whitney layer.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_sum_ofReal_collarCellForm_layer_le_framedMeanFourth_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (hstep : hn n ≤ hn (n + 1) + 1) (hgap : hn (n + 1) ≤ hn n + 1) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m0) {L : ℤ} (hmL : m ≤ L) {b Cgrad : ℝ} (hCgrad : 1 ≤ Cgrad) (hb : 0 ≤ b) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (Fv Gv : Whitney.KuhnCell d → HCPolySupport.Vec d) (p : HCPolySupport.Vec d), (∀ Q ∈ Whitney.whitneyLayer m hn n, ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, HCPolySupport.vecNormSq (Fv T - p) ≤ Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n)))) * HCPolySupport.vecNormSq p) → (∀ Q ∈ Whitney.whitneyLayer m hn n, ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, HCPolySupport.vecNormSq (Gv T) ≤ 0) → ∑ Q ∈ collarLayer M m hn n omega, ∑ T ∈ Whitney.whitneySimplexCells m hn n Q, ENNReal.ofReal (cellWeight m T * collarCellForm M m hn L omega (fun (U : Whitney.KuhnCell d) => (√↑(Annealed.sigmaBar M i))⁻¹ • Fv U) (fun (U : Whitney.KuhnCell d) => √↑(Annealed.sigmaBar M i) • Gv U) T) ≤ ENNReal.ofReal (probeFramedCollarLayerMeanRhs M m hn n i L omega p Cgrad b)

Internal conditional aggregation of the framed potential majorant over a collar Whitney layer.