StepSixBoundaryEndpoint #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The composition, with the flat leg held out #
theorem
Algsuperdiff.Section4.Provider.Regularity.holderBoundary_compose
{C E R A oscLo oscHi dataG dataHs Fl : ℝ}
(hC : 0 ≤ C)
(hE : 0 ≤ E)
(hER : E ≤ R)
(hoscHi : 0 ≤ oscHi)
(hdataG : 0 ≤ dataG)
(hdataHs : 0 ≤ dataHs)
(habs : E * Fl ≤ A)
(hiter : oscLo ≤ C * E * (oscHi + C * dataG) + C * E * (dataHs + Fl))
:
Step 6 with a held-out flat leg. The prefactor is replaced by R on the
geometric part, while the flat part Fl is absorbed separately (habs),
because absorption consumes the exponential itself.
theorem
Algsuperdiff.Section4.Provider.Regularity.stepSixBoundary_holderBound_epsFunded
(d : ℕ)
{Cedos Cann Citer C alpha : ℝ}
{k : ℕ}
{n m : ℤ}
{oscLo oscHi dataG Khleg Hinf ind Se : ℝ}
(hC : 0 ≤ C)
(hCiter : 0 ≤ Citer)
(halpha : alpha ≤ 1)
(hnm : n ≤ m)
(hoscHi : 0 ≤ oscHi)
(hdataG : 0 ≤ dataG)
(hKhleg : 0 ≤ Khleg)
(hHinf : 0 ≤ Hinf)
(hind : 0 ≤ ind)
(hSe0 : 0 ≤ Se)
(hSe : Se ≤ 2 * stepOneDelta (stepOneC1 d Cedos Cann Citer k) alpha * (↑m - ↑n))
(hiter :
oscLo ≤ C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * (oscHi + C * dataG) + C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * ((Khleg + Se * Hinf) * ind))
:
e.oscillation.Holder.bound on the boundary branch, as the print builds
it.
The flat ∇h leg enters δ_j with the coefficient ε_j, so its window sum is
S_ε ≤ 2 δ (m-n) = 2 C₁^{-1}(1-α)(m-n); the absorption t e^t ≤ e^{2t} then
delivers it at the printed exponent with the ABSOLUTE constant 4/log 3:
oscLo ≤ (C+C²) 3^{(1/2)(1-α)(m-n)} ( oscHi + dataG + K_h-leg · 1 )
+ C (4/log 3) 3^{(1/2)(1-α)(m-n)} ( ‖∇h‖_{L^∞} · 1 ) .