SharpFramedMeanCells

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

Cellwise carriers for the framed simplex-mean majorant

This file transports probeFramedMeanCellMajorant through the Whitney good-cell and collar carriers. Every result below is an internal conditional proof obligation.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_blockVecDot_simplexDomain_le_framedMeanMajorant_ae_uniform {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (Q : HCPolySupport.TriadicCube d) (k i : ℤ), Q.scale ≤ i → i ≤ m₀ → omega ∉ BadEvents.badOsc M Q → omega ∉ BadEvents.badLoc M Q → ∀ (L : ℤ), Q.scale ≤ L → ∀ (T : Whitney.KuhnCell d), T.supportCube ∈ HCPolySupport.descendantsAtScale Q k → ∀ (p q : HCPolySupport.Vec d), HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T)) ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q)) ≤ probeFramedMeanCellMajorant M Q k i L omega T p q

Internal conditional A for uniformizing the framed simplex-domain bound over all cubes and two running scales.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_blockVecDot_whitneySimplexCells_le_framedMeanMajorant_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (m : ℤ) (hn : ℕ → ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m₀) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, omega ∉ BadEvents.bad M Q → ∀ (L : ℤ), Q.scale ≤ L → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ∀ (p q : HCPolySupport.Vec d), HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T)) ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q)) ≤ probeFramedMeanCellMajorant M Q (Whitney.simplexScale m hn n) i L omega T p q

Internal conditional A for applying the framed cell majorant to Whitney simplex cells.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_goodCellForm_le_framedMeanMajorant_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (m : ℤ) (hn : ℕ → ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m₀) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, ∀ (L : ℤ), Q.scale ≤ L → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ∀ (p q : HCPolySupport.Vec d), goodCellForm M m hn L omega ((√↑(Annealed.sigmaBar M i))⁻¹ • p) (√↑(Annealed.sigmaBar M i) • q) T ≤ probeFramedMeanCellMajorant M Q (Whitney.simplexScale m hn n) i L omega T p q

Internal conditional A for the framed majorant on goodCellForm.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_blockVecDot_collar_simplexDomain_le_framedMeanMajorant_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (m : ℤ) (hn : ℕ → ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m₀) {b Cgrad : ℝ} (hCgrad : 1 ≤ Cgrad) (hb : 0 ≤ b) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, omega ∉ BadEvents.bad M Q → ∀ (L : ℤ), Q.scale ≤ L → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ∀ (p q Fv Gv : HCPolySupport.Vec d), HCPolySupport.vecNormSq (Fv - p) ≤ Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n)))) * HCPolySupport.vecNormSq p → HCPolySupport.vecNormSq (Gv - q) ≤ Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n)))) * HCPolySupport.vecNormSq q → HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • Fv, √↑(Annealed.sigmaBar M i) • Gv) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T)) ((√↑(Annealed.sigmaBar M i))⁻¹ • Fv, √↑(Annealed.sigmaBar M i) • Gv)) ≤ 4 * (Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n))))) * probeFramedMeanCellMajorant M Q (Whitney.simplexScale m hn n) i L omega T p q

Internal conditional A for the framed majorant on the collar simplex quadratic form.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_collarCellForm_le_framedMeanMajorant_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (m : ℤ) (hn : ℕ → ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m₀) {b Cgrad : ℝ} (hCgrad : 1 ≤ Cgrad) (hb : 0 ≤ b) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, ∀ (L : ℤ), Q.scale ≤ L → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ∀ (Fv Gv : Whitney.KuhnCell d → HCPolySupport.Vec d) (p q : HCPolySupport.Vec d), HCPolySupport.vecNormSq (Fv T - p) ≤ Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n)))) * HCPolySupport.vecNormSq p → HCPolySupport.vecNormSq (Gv T - q) ≤ Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n)))) * HCPolySupport.vecNormSq q → 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 ≤ 4 * (Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n))))) * probeFramedMeanCellMajorant M Q (Whitney.simplexScale m hn n) i L omega T p q

Internal conditional A for the framed majorant on collarCellForm.