HomCGFinalFullNorm

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

The FULL W^{s′,q} norm of a Hölder field, against the test gauge

What this file supplies

HomCGFinalGagliardo bounds the seminorm half of CoarseGraining's cubeEuclideanWspFullENorm. This file adds the L^{q} half — a sup bound is enough, because the underlying measure is the NORMALIZED cube measure, a probability measure — and assembles both against the Step-4 test gauge wsInftyGauge.

The L^{q} half carries the scale weight cubeEuclideanWspScalePowerWeight, i.e. L^{-s′q}; its q-th root is L^{-s′}. With L = 3^{m} the side, this is where the predicted single factor comes from:

  ‖φ‖_{W^{s′,q} full}  ≤  L^{-s′}·d·K_sup  +  d·C(d,β)^{1/q}·L^{α-s′}·K_Höl
                       ≤  K_test · ( L^{-α} K_sup + K_Höl )

with

  K_test  =  d · L^{α-s′} · (1 + C(d,β)^{1/q}),     β = d - (α-s′)q,

because L^{-s′} = L^{α-s′}·L^{-α}. The right-hand factor is exactly wsInftyGauge Q α K_sup K_Höl, whose L^∞ weight 3^{-α·scale} IS L^{-α}.

So the entire order loss α - s′ > 0 is paid as the single explicit factor L^{α-s′} = 3^{m(α-s′)} in cgTestConst, exactly as the measurement predicted, and nothing else about the two orders enters.

1. The cube side in the 3-gauge

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_neg_scale_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (alpha : ℝ) : Real.rpow 3 (-(alpha * ↑Q.scale)) = HCPolySupport.cubeScaleFactor Q ^ (-alpha)

The test gauge's L^∞ weight is the side to the power -α.

2. The L^{q} half of the full norm

theorem Algsuperdiff.Section4.Provider.Homogenization.normalizedEuclideanLpENorm_le_of_bound {d : ℕ} {Q : HCPolySupport.TriadicCube d} {r : ENNReal} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} {B : ℝ} (hF : ∀ (x : HCPolySupport.Vec d), ‖F x‖ ≤ B) (hFm : MeasureTheory.AEStronglyMeasurable (fun (x : HCPolySupport.Vec d) => HCPolySupport.euclideanNorm (F x)) (HCPolySupport.cubeBoundedMeasurableDomain Q).normalizedVolume) : (HCPolySupport.cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm r F ≤ ENNReal.ofReal (↑d * B)

A sup bound bounds the normalized L^{q} norm, at the dimensional constant of the Euclidean/supremum comparison and with NO measure factor: the normalized cube measure is a probability measure.

3. The full norm of a Hölder field

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeEuclideanWspFullENorm_le_of_holder {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s' : ↑HCPolySupport.FractionalOrder} {q : HCPolySupport.FiniteLpExponent} {phi : HCPolySupport.Vec d → HCPolySupport.Vec d} {alpha Ksup KHol : ℝ} (hKHol : 0 ≤ KHol) (hlo : 0 < (alpha - ↑s') * q.exponent.toReal) (hhi : (alpha - ↑s') * q.exponent.toReal < ↑d) (hsup : ∀ (x : HCPolySupport.Vec d), ‖phi x‖ ≤ Ksup) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet Q) alpha KHol phi) : HCPolySupport.cubeEuclideanWspFullENorm Q s' q phi ≤ ENNReal.ofReal (HCPolySupport.cubeScaleFactor Q ^ (-↑s') * (↑d * Ksup)) + ENNReal.ofReal (↑d * KHol * Regularity.radialKernelConst d (cgGagliardoBeta d alpha (↑s') q.exponent.toReal) ^ q.exponent.toReal⁻¹ * HCPolySupport.cubeScaleFactor Q ^ (alpha - ↑s'))

C^{0,α}(□) ⊂ W^{s′,q}(□) at the FULL norm.

4. The test constant, and the gauge comparison

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.cgTestConst (d : ℕ) (Q : HCPolySupport.TriadicCube d) (alpha s' t : ℝ) : ℝ

The test-class constant of the order-loss route. K_test(Q, α, s′, q) = d · L^{α-s′} · (1 + C(d, β)^{1/q}), β = d - (α-s′)q.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.cgTestConst_def (d : ℕ) (Q : HCPolySupport.TriadicCube d) (alpha s' t : ℝ) : cgTestConst d Q alpha s' t = ↑d * HCPolySupport.cubeScaleFactor Q ^ (alpha - s') * (1 + Regularity.radialKernelConst d (cgGagliardoBeta d alpha s' t) ^ t⁻¹)

theorem Algsuperdiff.Section4.Provider.Homogenization.cgTestConst_nonneg (d : ℕ) (Q : HCPolySupport.TriadicCube d) {alpha s' t : ℝ} (hlo : 0 < (alpha - s') * t) : 0 ≤ cgTestConst d Q alpha s' t

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeEuclideanWspFullENorm_le_gauge {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s' : ↑HCPolySupport.FractionalOrder} {q : HCPolySupport.FiniteLpExponent} {phi : HCPolySupport.Vec d → HCPolySupport.Vec d} {alpha Ksup KHol : ℝ} (hKsup : 0 ≤ Ksup) (hKHol : 0 ≤ KHol) (hlo : 0 < (alpha - ↑s') * q.exponent.toReal) (hhi : (alpha - ↑s') * q.exponent.toReal < ↑d) (hsup : ∀ (x : HCPolySupport.Vec d), ‖phi x‖ ≤ Ksup) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet Q) alpha KHol phi) : HCPolySupport.cubeEuclideanWspFullENorm Q s' q phi ≤ ENNReal.ofReal (cgTestConst d Q alpha (↑s') q.exponent.toReal * wsInftyGauge Q alpha Ksup KHol)

The full norm of a Hölder test field, against the Step-4 test gauge.

This is the honest, order-losing form of the smooth-dual/Hölder test comparison: the W^{s′,q} unit-ball gauge of a C^{0,α} field is at most K_test times its W^{α,∞} gauge, with K_test carrying the single factor 3^{m(α-s′)}.