Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Homogenization.HomSeamFluxHalfLevel

HomSeamFluxHalfLevel #

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

hlevelDual at the Schauder provenance α = 1/2 #

What this file supplies #

HomSeamFluxFreeCcg's hlevelDual at a free Ccg, with the Hölder gauge of the Step-4 test moved from α = s to α = 1/2, the dual order s′ = 7s/8 UNCHANGED. Nothing in the pairing chain notices: HomSpineInstallArith's hlevelDual_of_energyBound is already general in α (its s slot enters only through cgTestConstBase d s s′ t and the matching scale power), and cgTestConst_mul_rpow_originCube — the dual-order cancellation — is stated at general α too.

The visible change is the scale power on the right: at α = s the display carried 3^{sm}; at α = 1/2 it carries the print's own 3^{m/2} bracket (the printed display's Schauder weight 3^{m(1/2-s)} composed with the display's 3^{s′m}). In symbols, cgTestConst supplies the single factor 3^{m(α-s′)}, so

  cgTestConst □_m α s′ p′ · 3^{s′m}  =  cgTestConstBase d α s′ p′ · 3^{αm},

and at α = 1/2 the right side is K_test · 3^{m/2}.

Why this is the print's reading #

The Step-4 pairing tests against ∇v, the gradient of the constant-coefficient comparator, and the ONLY regularity the print has for it is the C^{0,1/2} Schauder estimate (the same estimate whose constant HomSchauderUniform.stepFourSchauderConstU already interpolates through). Reading the dual bound at order 1/2 rather than at order s therefore costs nothing at the consumption site — ∇v is in the smaller test class — while it removes the only closing order gap in the test-class conversion.

1. The Schauder gauge order #

source
noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutOrderHalf :
↑HCPolySupport.FractionalOrder

The print's Step-4 Hölder gauge, α = 1/2, as a FractionalOrder.

Equations
Instances For
    source
    @[simp]
    theorem Algsuperdiff.Section4.Provider.Homogenization.recutOrderHalf_val :
    ↑recutOrderHalf = 1 / 2
    source
    theorem Algsuperdiff.Section4.Provider.Homogenization.cgOrderWindow_half (p : HCPolySupport.FiniteLpExponent) {s : ℝ} (hquarter : s ≤ 1 / 4) :
    0 < (1 / 2 - 7 * s / 8) * p.conjugate.exponent.toReal

    The conversion window at the re-pin: the order gap 1/2 - 7s/8 is positive for every base order s ≤ 1/4, at every finite dual exponent.

    2. hlevelDual at α = 1/2 #

    source
    theorem Algsuperdiff.Section4.Provider.Homogenization.hlevelDualHalfFluxAt_of_seam {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L : ℤ) (omega : Section3.Cutoff.CutoffSample d) (m : ℤ) (jn : ℕ) {sigmaBarM : ℝ} (hsig : 0 < sigmaBarM) {Cgap : ℝ} (Y : Section3.Cutoff.CutoffSample d → ENNReal) (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Ccg Kg Kh KhInf S Cen0 Ktest : ℝ} (hCcg0 : 0 ≤ Ccg) (hs : 0 < homS M) (hlog : 4 ≤ |Real.log M.gamma|) (hgamma1 : M.gamma < 1) (hCgap : 0 < Cgap) (hss2 : homS M < ↑s2) (hs2lt : ↑s2 < 1 / 2) (hs2gt : 1 / 2 - ↑d / p.exponent.toReal < ↑s2) (hs2gap : 5 < 10 * ↑s2 * Real.log 3) (hKtest : Ktest = cgTestConstBase d (1 / 2) (7 * homS M / 8) p.conjugate.exponent.toReal) (hKg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g) (hKhInf0 : 0 ≤ KhInf) (hKh0 : 0 ≤ Kh) (hCen0 : 0 ≤ Cen0) (hjn : (HCPolySupport.originCube d m).scale - ↑jn = homN M m) (hSbound : S ≤ Cen0 * recutEnergyFactor M Y m omega * energyBracket sigmaBarM (Real.rpow 3 (↑m / 2)) Kg KhInf Kh) (hdom1 : ENNReal.ofReal (recutPinnedE1Flux M L omega m jn hsig (recutOrderBase M hlog)) ≤ Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homHalf (homSeamBase M hs)) omega) (hdom2 : ENNReal.ofReal (recutPinnedE2Flux M L omega m jn hsig (recutOrderBase M hlog)) ≤ ENNReal.ofReal √2 * Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homQuarterOf (homSeamBase M hs)) omega) (hfin : ethmB M Cgap Y m (homN M m) (homSeamBase M hs) omega ≠ ⊤) :
    cgTestConst d (HCPolySupport.originCube d m) (1 / 2) (7 * ↑(recutOrderBase M hlog) / 8) p.conjugate.exponent.toReal * (Real.rpow 3 (7 * ↑(recutOrderBase M hlog) / 8 * ↑m) * coarseGrainingFinitePRHS Ccg (7 * ↑(recutOrderBase M hlog) / 8) (↑s2) sigmaBarM (recutPinnedE1Flux M L omega m jn hsig (recutOrderBase M hlog)) (recutPinnedE2Flux M L omega m jn hsig (recutOrderBase M hlog)) (recutPinnedDg m s2 p g) S ((HCPolySupport.originCube d m).scale - ↑jn)) ≤ Real.rpow 3 (1 / 2 * ↑m) * (sigmaBarM * (2 * pairCwOf d Ccg p s2 Cgap Cen0 (homS M) Ktest * (ethmB M Cgap Y m (homN M m) (homSeamBase M hs) omega).toReal * dataBracket sigmaBarM (Real.rpow 3 (↑m / 2)) Kg KhInf Kh))

    hlevelDual AT THE SCHAUDER PROVENANCE α = 1/2, A FREE Ccg, THE ã COEFFICIENT AND THE BASE s/8.

    HomSeamFluxFreeCcg's hlevelDual at a free Ccg, with the test's Hölder gauge re-pinned. Two hypotheses of the sibling are GONE (1 ≤ d and the guard s + d/p ≤ 1/2): they were needed only to place the closing order gap α - s′ = s/8 inside the Gagliardo window, and the fixed gap 1/2 - 7s/8 is inside it for free.