HomCGFinalDatum

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

The printed data hypothesis 𝐠 ∈ W^{s₂,p}(□_m), from the root's own binder

What this file supplies

The measurement named ONE printed hypothesis the spine's bundle does not carry: the coarse-graining display's data membership 𝐠 ∈ W^{s₂,p}(□_m). It is not an extra assumption — it follows from the root's OWN C^{0,1/2} binder on 𝐠, which the spine already quantifies, by the same embedding HomCGFinalGagliardo supplies, read at (α, s′) = (1/2, s₂).

• memCubeEuclideanFullWsp_of_holder — the general statement;
• memCubeEuclideanFullWsp_of_holderHalf — the pinned instance at α = 1/2;
• holderHalf_window — the admissible s₂ band: 1/2 - d/p < s₂ < 1/2.

At the pin p = 4d the band is 1/4 < s₂ < 1/2, which is compatible with the bundle's own s < s₂ < 1 whenever s < 1/4 — and the bundle's guard s + d/p ≤ 1/2 gives exactly s ≤ 1/4 at that pin. The band is nonempty and s₂ is existentially quantified by the bundle, so nothing is over-determined.

The two subtype bridges

mkFractionalOrder and mkFiniteLpExponent build CoarseGraining's carriers from raw reals; both come with the toReal computation, so a consumer working with the manuscript's numerals never has to unfold a subtype.

2. The L^p half from the Hölder binder

theorem Algsuperdiff.Section4.Provider.Homogenization.memLp_ofVec_of_holderSeminormBoundOn_originCube {d : ℕ} {m : ℤ} {alpha K : ℝ} {p : HCPolySupport.FiniteLpExponent} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (halpha : 0 < alpha) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) alpha K g) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (g x)) p.exponent (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d m))

A C^{0,α} field on □_m is in L^p of the normalized cube measure.

3. The full fractional membership

theorem Algsuperdiff.Section4.Provider.Homogenization.memCubeEuclideanFullWsp_of_holder {d : ℕ} {m : ℤ} {s2 : ↑HCPolySupport.FractionalOrder} {p : HCPolySupport.FiniteLpExponent} {alpha K : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (halpha : 0 < alpha) (hlo : 0 < (alpha - ↑s2) * p.exponent.toReal) (hhi : (alpha - ↑s2) * p.exponent.toReal < ↑d) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) alpha K g) : HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp (HCPolySupport.originCube d m) s2 p g

C^{0,α}(□_m) ⊂ W^{s₂,p}(□_m), at CoarseGraining's membership predicate.

theorem Algsuperdiff.Section4.Provider.Homogenization.holderHalf_window {d : ℕ} {p : HCPolySupport.FiniteLpExponent} {s2 : ℝ} (hlt : s2 < 1 / 2) (hgt : 1 / 2 - ↑d / p.exponent.toReal < s2) : 0 < (1 / 2 - s2) * p.exponent.toReal ∧ (1 / 2 - s2) * p.exponent.toReal < ↑d

The admissible s₂ band at the Hölder exponent 1/2.

theorem Algsuperdiff.Section4.Provider.Homogenization.memCubeEuclideanFullWsp_of_holderHalf {d : ℕ} {m : ℤ} {s2 : ↑HCPolySupport.FractionalOrder} {p : HCPolySupport.FiniteLpExponent} {K : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (hlt : ↑s2 < 1 / 2) (hgt : 1 / 2 - ↑d / p.exponent.toReal < ↑s2) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K g) : HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp (HCPolySupport.originCube d m) s2 p g

The pinned instance: the root's own C^{0,1/2} binder on 𝐠 supplies the printed data hypothesis 𝐠 ∈ W^{s₂,p}(□_m).