HomCGFinalTestClass

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

The test-class conversion, at the two orders s′ < s

What this file supplies

The domination of the Hölder test gauge by CoarseGraining's smooth W^{s,p′} dual is the ONE gap between that dual and the repository's WeakNegDualBoundOn, and it is FALSE at equal orders (the Gagliardo integrand of a C^{0,s} field is logarithmically divergent). This file gives the honest, order-losing form as a THEOREM:

  SmoothDualDominatesHolderTestsAt Q s′ s p (cgTestConst d Q s s′ p′)

for every pair s′ < s in the admissible window 0 < (s-s′)p′ < d. The constant is HomCGFinalFullNorm's, i.e. d·3^{m(s-s′)}·(1 + C(d,β)^{1/p′}), and the two orders enter ONLY through that single factor.

The route, in one line

A merely Hölder test φ is not admissible against the smooth dual, which is a supremum over globally C^∞ unit tests. Normalize φ by the gauge (ψ = φ / (K_test · gauge)), extend it by McShane and mollify it (HomCGFinalSmoothTest): the resulting fields are globally smooth, carry the SAME two constants, and hence sit in the unit ball of cubeEuclideanWspFullENorm by HomCGFinalFullNorm.cubeEuclideanWspFullENorm_le_gauge. Each therefore pairs against F below the dual norm D. They converge to ψ pointwise on the open cube, and F ∈ L² of a probability measure dominates the pairing integrand uniformly, so dominated convergence transports the bound to ψ itself, i.e. to |⟨F, φ⟩| ≤ D · K_test · gauge.

What it costs, and why it is free at the level

Nothing is paid at the level: cgTestConst carries 3^{m(s-s′)} and the smooth-dual display at order s′ carries 3^{s′m}, so the product is 3^{sm}, the level the Step-4 consumer wants. The order loss is paid only inside the printed right-hand side, whose s^{-1}, s^{-9/2} and (s₂-s)^{-1} are read at s′; the spine's bundle quantifies all of those existentially.

1. The cube pairing as an integral against the normalized cube measure

theorem Algsuperdiff.Section4.Provider.Homogenization.normalizedCubeMeasure_eq_smul_restrict_openCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.normalizedCubeMeasure Q = (MeasureTheory.volume (HCPolySupport.openCubeSet Q))⁻¹ • MeasureTheory.volume.restrict (HCPolySupport.openCubeSet Q)

The normalized cube measure, realized on the OPEN cube.

theorem Algsuperdiff.Section4.Provider.Homogenization.cubePairing_eq_integral {d : ℕ} (Q : HCPolySupport.TriadicCube d) (F psi : HCPolySupport.Vec d → HCPolySupport.Vec d) : cubePairing Q F psi = ∫ (x : HCPolySupport.Vec d), HCPolySupport.vecDot (F x) (psi x) ∂HCPolySupport.normalizedCubeMeasure Q

⨍_□ F·φ IS CoarseGraining's normalized pairing.

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_mem_openCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure Q, x ∈ HCPolySupport.openCubeSet Q

Almost every point of the normalized cube measure lies in the open cube.

theorem Algsuperdiff.Section4.Provider.Homogenization.cubePairing_const_smul_right {d : ℕ} (Q : HCPolySupport.TriadicCube d) (F psi : HCPolySupport.Vec d → HCPolySupport.Vec d) (c : ℝ) : (cubePairing Q F fun (x : HCPolySupport.Vec d) => c • psi x) = c * cubePairing Q F psi

The pairing is homogeneous in the test field.

2. The pairing integrand, dominated

3. The dominated-convergence transport of the pairing

theorem Algsuperdiff.Section4.Provider.Homogenization.tendsto_cubePairing {d : ℕ} {Q : HCPolySupport.TriadicCube d} (F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two) {psi : ℕ → HCPolySupport.Vec d → HCPolySupport.Vec d} {psiLim : HCPolySupport.Vec d → HCPolySupport.Vec d} {B : ℝ} (hint : ∀ (k : ℕ), MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F.toField x) (psi k x)) (HCPolySupport.normalizedCubeMeasure Q)) (hbound : ∀ (k : ℕ) (x : HCPolySupport.Vec d), ‖psi k x‖ ≤ B) (hlim : ∀ x ∈ HCPolySupport.openCubeSet Q, Filter.Tendsto (fun (k : ℕ) => psi k x) Filter.atTop (nhds (psiLim x))) : Filter.Tendsto (fun (k : ℕ) => cubePairing Q F.toField (psi k)) Filter.atTop (nhds (cubePairing Q F.toField psiLim))

The pairing passes to a uniformly bounded pointwise limit of test fields.

4. A smooth unit test pairs below the dual norm

theorem Algsuperdiff.Section4.Provider.Homogenization.ofReal_abs_cubePairing_le_dual {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s' : ↑HCPolySupport.FractionalOrder} {p : HCPolySupport.FiniteLpExponent} (F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two) (h : HCPolySupport.CubeEuclideanWspSmoothTest Q s' p.conjugate) (hle : HCPolySupport.cubeEuclideanWspFullENorm Q s' p.conjugate h.toField ≤ 1) : ENNReal.ofReal |cubePairing Q F.toField h.toField| ≤ HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm Q s' p F

Every smooth field in the unit ball pairs below the smooth dual norm.

5. The open cube is nonempty

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeCenter_mem_openCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeCenter Q ∈ HCPolySupport.openCubeSet Q

The centre of a triadic cube lies in its open realization.

theorem Algsuperdiff.Section4.Provider.Homogenization.openCubeSet_nonempty {d : ℕ} (Q : HCPolySupport.TriadicCube d) : (HCPolySupport.openCubeSet Q).Nonempty

6. The two-order test-class comparison

def Algsuperdiff.Section4.Provider.Homogenization.SmoothDualDominatesHolderTestsAt {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s' s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (Ktest : ℝ) : Prop

The test-class comparison at the two orders s′ (dual) and s (data).

This is the smooth-dual/Hölder test domination with the CoarseGraining side read at the strictly smaller order s′, which is the only reading that can be true.

Equations

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

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

The test constant is strictly positive in the admissible window.

theorem Algsuperdiff.Section4.Provider.Homogenization.smoothDualDominatesHolderTestsAt {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s' s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (hlo : 0 < (↑s - ↑s') * p.conjugate.exponent.toReal) (hhi : (↑s - ↑s') * p.conjugate.exponent.toReal < ↑d) : SmoothDualDominatesHolderTestsAt Q s' s p (cgTestConst d Q (↑s) (↑s') p.conjugate.exponent.toReal)

THE TEST-CLASS COMPARISON, LANDED.

7. The WeakNegDualBoundOn conversion at the two orders

theorem Algsuperdiff.Section4.Provider.Homogenization.weakNegDualBoundOn_of_smoothDualAt {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s' s : ↑HCPolySupport.FractionalOrder} {p : HCPolySupport.FiniteLpExponent} {Ktest : ℝ} (hK : 0 ≤ Ktest) (hclass : SmoothDualDominatesHolderTestsAt Q s' s p Ktest) {F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two} {D : ℝ} (hD : 0 ≤ D) (hF : HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm Q s' p F ≤ ENNReal.ofReal D) : WeakNegDualBoundOn Q (↑s) (Ktest * D) F.toField

The Step-4 carrier, produced from the smooth-dual level at order s′.

The conversion of a smooth-dual level into the Step-4 carrier, with the CoarseGraining side read at s′ < s. The output level is the data order s, which is what the bundle's duality clauses use.