SharpFramedPotentialProfile

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

Framed sharp upper-potential bounds from the profile gate

These declarations discharge the raw bad-event gates of the framed potential producers from the profile maximum and fifth-root hypotheses. In particular, none of these declarations certifies any source step or any fraction of one.

theorem Algsuperdiff.Section3.Provider.Multiscale.descendant_cutoffBlock_le_meanEnvelope_ae_of_profileGate {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (CoarseEllipticity.profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) {k₀ : ℕ} (hk₀ : 3 ≤ k₀) {L : ℤ} (hL : m - 1 ≤ L) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ENNReal.ofReal (CoarseEllipticity.cutoffBBlockFamily M L (↑(Annealed.sigmaBar M (m - 1)))⁻¹ R omega) ≤ ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (probeSharpFramedMeanLayerEnvelope M R.scale (↑E) CoarseEllipticity.bfaProfileB k₀ n (m - 1) L (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) (HCPolySupport.basisVec j) (Affine.superposedGradConst d))

At a fixed strict descendant, the translated framed sharp envelope follows from the profile gates.