StepFourCollapseErrorWeighted

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

1. The 𝓔-multiplied flat leg

theorem Algsuperdiff.Section4.Provider.Regularity.edLeg_four_le_errorWeighted {n : ℤ} {Cst s Efl Hl2 epsj Khinf : ℝ} (hcoef : 0 ≤ Cst * s ^ (-6)) (hEfl0 : 0 ≤ Efl) (hEfl : Efl ≤ epsj) (hKhinf : 0 ≤ Khinf) (hHl2 : Hl2 ≤ Khinf) : 3 ^ (-n) * (Cst * s ^ (-6) * Efl * 3 ^ ↑(n - 2) * Hl2) ≤ Cst * s ^ (-6) * epsj * (1 / 9 * Khinf)

The L²-datum leg conversion.

The error-weighted general clause states its flat ∇h leg 𝓔-multiplied, so the excess-decay display's fourth leg reads C s^{-6} · 𝓔 · 3^{n-2} · Hl2. The flat weight is edLeg_four_le's own 3^{-n} 3^{n-2} = 1/9; what is new is that the 𝓔 factor is spent against 𝓔 ≤ ε_j, so the leg is delivered with ε_j in place of 𝓔.

2. The bracket bound

theorem Algsuperdiff.Section4.Provider.Regularity.edBracket_le_errorWeighted {n : ℤ} {Crem Vd Cst s Efl Osc Gav Gsem Hsem Hl2 SigInv SigInvN epsj Kg Kh Khinf Cosc E0 S0 : ℝ} (hCV : 0 ≤ Crem * Vd) (hs : 0 ≤ s) (hcoef4 : 0 ≤ Cst * s ^ (-4)) (hcoef6 : 0 ≤ Cst * s ^ (-6)) (hcoef7 : 0 ≤ Cst * s ^ (-7)) (hw : 0 ≤ s ^ (-(3 / 2))) (hEfl0 : 0 ≤ Efl) (hEfl : Efl ≤ epsj) (heps0 : 0 ≤ epsj) (hOsc0 : 0 ≤ 3 ^ (-n) * Osc) (hOsc : 3 ^ (-n) * Osc ≤ Cosc * (E0 + S0)) (hGav0 : 0 ≤ Gav) (hGav : Gav ≤ Khinf) (hSig : SigInv ≤ 8 * SigInvN) (hSigN0 : 0 ≤ SigInvN) (hGsem0 : 0 ≤ Gsem) (hKg0 : 0 ≤ Kg) (hGsem : Gsem ≤ Kg * 3 ^ (↑(n + 1) * (1 / 2 - s))) (hKh0 : 0 ≤ Kh) (hHsem : Hsem ≤ Kh * 3 ^ (↑(n + 1) * (1 / 2 - s))) (hHl2 : Hl2 ≤ Khinf) : Crem * (3 ^ (-n) * (Vd * (Cst * s ^ (-4) * Efl * (Osc + s ^ (-(3 / 2)) * 3 ^ ↑(n - 2) * Gav) + Cst * s ^ (-7) * SigInv * 3 ^ ((1 + s) * ↑(n - 2)) * Gsem + Cst * s ^ (-6) * 3 ^ ((1 + s) * ↑(n - 2)) * Hsem + Cst * s ^ (-6) * Efl * 3 ^ ↑(n - 2) * Hl2))) ≤ stepFourEpsCoeff Crem Vd Cst s Cosc * epsj * E0 + (stepFourEpsCoeff Crem Vd Cst s Cosc * epsj * S0 + stepFourDeltaOutErrorWeighted Crem Vd Cst s epsj Khinf SigInvN Kg Kh n)

The bracket bound: the whole excess-decay remainder at the error-weighted clause, split into the absorbable contraction (C_ε ε_j) E, the ε_j |∇ℓ| leg, and δ_n in its stepFourDeltaOutErrorWeighted shape. Legs one, two and three are verbatim; only the fourth is re-run.