Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Multiscale.SharpFramedSimplexMean

SharpFramedSimplexMean #

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

The framed upper Step-1 simplex estimate #

This file retains the factor 3^(-gamma * (i - j)) when the normalized potential response is estimated at a fine cube of scale j and observation scale i. The factor comes from applying the growth branch of the induction window at both running-diffusivity indices.

The results below are internal conditional proof obligations.

source
theorem Algsuperdiff.Section3.Provider.Multiscale.probe_responseJ_simplexDomain_normalized_flux_le_framed_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (Q : HCPolySupport.TriadicCube d) (hm : Q.scale ≤ m₀) (k : ℤ) {i : ℤ} (hji : Q.scale ≤ i) (hi : i ≤ m₀) :
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw 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 : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.responseJ (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T) ((√↑(Annealed.sigmaBar M i))⁻¹ • p) 0 ≤ 160 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k (1 / 4) * (1 + 8 * BadEvents.bigLambdaSensitivityConst d * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑Q.scale)) * 3 ^ (-(M.gamma * ↑(i - Q.scale))) * (BadEvents.incrementUnitCube₂ Q Q.scale L omega).w1Infinity ^ 2) * HCPolySupport.vecNormSq p

The normalized potential response with the global depth frame retained in the increment term.

source
theorem Algsuperdiff.Section3.Provider.Multiscale.probe_responseJ_simplexDomain_normalized_flux_le_framed_simplexMean_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (Q : HCPolySupport.TriadicCube d) (hm : Q.scale ≤ m₀) (k : ℤ) {i : ℤ} (hji : Q.scale ≤ i) (hi : i ≤ m₀) :
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw 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 : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.responseJ (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T) ((√↑(Annealed.sigmaBar M i))⁻¹ • p) 0 ≤ 160 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k (1 / 4) * (1 + probeSimplexMeanSensitivityConst d * BadEvents.deltaOsc d ^ 2 + probeSimplexMeanSensitivityConst d * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑Q.scale)) * 3 ^ (-(M.gamma * ↑(i - Q.scale))) * HCPolySupport.Book.Ch02.matrixOperatorNorm (simplexIncrementValue Q.scale L (↑omega) T) ^ 2) * HCPolySupport.vecNormSq p

The preceding framed response estimate after replacing the increment supremum by its simplex mean and oscillation threshold. Only the random simplex-mean term retains the frame; the deterministic threshold term uses that the frame is at most one.

source
theorem Algsuperdiff.Section3.Provider.Multiscale.probe_blockVecDot_coarseBlockMatrix_simplexDomain_le_framedMean_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (Q : HCPolySupport.TriadicCube d) (hm : Q.scale ≤ m₀) (k : ℤ) {i : ℤ} (hji : Q.scale ≤ i) (hi : i ≤ m₀) :
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw 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)) ≤ 640 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k (1 / 4) * (1 + probeSimplexMeanSensitivityConst d * BadEvents.deltaOsc d ^ 2 + probeSimplexMeanSensitivityConst d * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑Q.scale)) * 3 ^ (-(M.gamma * ↑(i - Q.scale))) * HCPolySupport.Book.Ch02.matrixOperatorNorm (simplexIncrementValue Q.scale L (↑omega) T) ^ 2) * HCPolySupport.vecNormSq p + 320 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k (1 / 4) * 3 ^ (M.gamma * (↑i - ↑Q.scale)) * HCPolySupport.vecNormSq q

The full simplex quadratic form obtained by combining the framed potential leg with the unchanged normalized slope leg.

source
noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeFramedMeanCellMajorant {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (k i L : ℤ) (omega : Cutoff.CutoffSample d) (T : Whitney.KuhnCell d) (p q : HCPolySupport.Vec d) :
ℝ

Cellwise majorant whose random potential term retains the observation-to- cube scale frame.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.probeFramedMeanCellMajorant_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (k i L : ℤ) (omega : Cutoff.CutoffSample d) (T : Whitney.KuhnCell d) (p q : HCPolySupport.Vec d) :
    0 ≤ probeFramedMeanCellMajorant M Q k i L omega T p q
    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.probe_blockVecDot_coarseBlockMatrix_simplexDomain_le_framedMeanMajorant_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (Q : HCPolySupport.TriadicCube d) (hm : Q.scale ≤ m₀) (k : ℤ) {i : ℤ} (hji : Q.scale ≤ i) (hi : i ≤ m₀) :
    ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw 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