SharpMeanLayerEnvelope

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpMeanAffine (B C mass wave : ℝ) : ℝ

The affine mass-plus-wave expression used to compare sharp mean budgets.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.probeSharpMeanAffine B C mass wave = B * mass + C * √mass * wave

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpMeanAffine_mono {B C mass mass' wave wave' : ℝ} (hB : 0 ≤ B) (hC : 0 ≤ C) (hwave : 0 ≤ wave) (hmass_le : mass ≤ mass') (hwave_le : wave ≤ wave') : probeSharpMeanAffine B C mass wave ≤ probeSharpMeanAffine B C mass' wave'

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerMassEnvelope (d n : ℕ) : ℝ

The geometric envelope for the mass of a Whitney layer.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerMassEnvelope d n = 6 * ↑d * 3 ^ (-↑n)

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

The five-term wave envelope used for one Whitney layer. The seam re-gauging factor is deliberately visible.

Equations

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