Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Regularity.RootInterfaceMerge

RootInterfaceMerge #

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

Projections of a merged threshold #

source
theorem Algsuperdiff.Section4.Provider.Regularity.rootGamma0_le_left {g0 g1 gamma : ℝ} (h : gamma ≤ min g0 g1) :
gamma ≤ g0

The left projection of a merged threshold.

source
theorem Algsuperdiff.Section4.Provider.Regularity.rootGamma0_le_right {g0 g1 gamma : ℝ} (h : gamma ≤ min g0 g1) :
gamma ≤ g1

The right projection of a merged threshold.

The boundary-leg-free a.e. display #

source
def Algsuperdiff.Section4.Provider.Regularity.RootDisplayClauseBAe {d : ℕ} (M : Section3.ABKModel d) (C1 Cest alpha : ℝ) :
Prop

Clause (B) of the a.e. lattice display: the boundary-leg-free estimate, gated by the off-grid centre belonging to □_{m-1}.

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

    Increasing the estimate constant #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.RootDisplayClauseBAe.mono_const {d : ℕ} [NeZero d] {M : Section3.ABKModel d} {C1 Cest Cest' alpha : ℝ} (hle : Cest ≤ Cest') (h : RootDisplayClauseBAe M C1 Cest alpha) :
    RootDisplayClauseBAe M C1 Cest' alpha