Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Multiscale.SharpFramedMeanLayerEnvelope

SharpFramedMeanLayerEnvelope #

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

Sharp Whitney-layer envelope with the global frame retained #

The framed simplex-mean wave contribution is bounded by multiplying the existing five-term sharp wave envelope by the observation-to-cube frame. The frame multiplies only the wave contribution, never the complete affine layer envelope.

These are internal conditional proof obligations.

source
noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerFrame {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (omega : Cutoff.CutoffSample d) :
ℝ

The generic layer frame specialized to the random Whitney scale.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedLayerWaveEnvelope {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) :
    ℝ

    The five-term sharp wave envelope with the specialized layer frame.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedMeanLayerEnvelope {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) (p : HCPolySupport.Vec d) (Cgrad : ℝ) :
      ℝ

      The good/collar affine layer envelope with only its wave argument replaced by the framed sharp wave envelope.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerFrame_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (omega : Cutoff.CutoffSample d) :
        0 ≤ probeSharpLayerFrame M m E b k₀ n i omega
        source
        theorem Algsuperdiff.Section3.Provider.Multiscale.probeFramedLayerWaveFactor_le_sharpFramedLayerWaveEnvelope {d : ℕ} (M : ABKModel d) {m : ℤ} {E b : ℝ} (hb₀ : 0 < b) (hb₁ : b ≤ 1 / 8) {k₀ : ℕ} (hk₀ : 2 ≤ k₀) (i : ℤ) {L : ℤ} (hmL : m ≤ L) (n : ℕ) (omega : Cutoff.CutoffSample d) :
        probeFramedLayerWaveFactor M m (Whitney.whitneyScale M m E b k₀ omega) n i L omega ≤ probeSharpFramedLayerWaveEnvelope M m E b k₀ n i L omega

        The specialized framed fourth-mass wave factor is bounded by the framed five-term sharp wave envelope.

        source
        theorem Algsuperdiff.Section3.Provider.Multiscale.probe_framedGood_add_collar_layer_rhs_le_sharpEnvelope {d : ℕ} (M : ABKModel d) {m : ℤ} {E b : ℝ} (hd : 2 ≤ d) (hb₀ : 0 < b) (hb₁ : b ≤ 1 / 8) {k₀ : ℕ} (hk₀ : 2 ≤ k₀) (i : ℤ) {L : ℤ} (hmL : m ≤ L) (n : ℕ) (omega : Cutoff.CutoffSample d) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (p : HCPolySupport.Vec d) (Cgrad : ℝ) :
        probeFramedGoodLayerMeanRhs M m (Whitney.whitneyScale M m E b k₀ omega) n i L omega p + probeFramedCollarLayerMeanRhs M m (Whitney.whitneyScale M m E b k₀ omega) n i L omega p Cgrad b ≤ probeSharpFramedMeanLayerEnvelope M m E b k₀ n i L omega p Cgrad