HomStepThreeData

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

Theorem B, §4.5: the residues M1, M2, M3

What Step 2 hands forward

The Step-2a display prices the §4.5 energy by CoarseGraining's Besov data quantities B_g, B_h. Converting those to the printed 3^{m/2} runs through the bridge ExcessDecay.scaleNormalizedPositiveBesovVectorSeminormTwo_le_gagliardo composed with the embedding HomBridgeDataEmbedding's pinned data embedding. The bridge has two side conditions that existed nowhere, and its ∇h leg carries a MEAN term that a Hölder seminorm alone cannot price. Those were M1, M2, M3. All three are settled here.

• (M1) MemLp g 2 (normalizedCubeMeasure □_m) from a Hölder-1/2 bound on the open cube (memLp_two_normalizedCubeMeasure_of_holderHalf). Route: the Hölder bound gives ContinuousOn (hence AEStronglyMeasurable on the restricted measure) and, against ANY one point of the cube, the pointwise bound ‖g x‖ ≤ ‖g 0‖ + K √(3^m); a bounded function on a finite measure is L^∞, hence L². This is the essential-sup route of the Step-5 data layer, run here at the L² exponent.
• (M2) Gagliardo.MemWsp □_m t 2 g (memWsp_of_holderHalf). Its eSeminorm < ⊤ half is the embedding atom read through ExcessDecay.normalizedGagliardoESeminormOn_openCubeSet; the genuinely new half is AEStronglyMeasurable (gagliardoKernel t 2 g) for the Gagliardo PRODUCT measure, which is obtained by the BoundsEaL-style measure algebra (normalizedGagliardoMeasureOn A = (vol A)⁻¹ • (volume.prod volume).restrict (A ×ˢ A), the own rewrite) plus CoarseGraining's own kernel-measurability idiom (measurable_dist.pow measurable_const, the scalar factor is GLOBALLY measurable; only the vector factor needs the window).
• (M1)+(M2) discharge ForceBesovRegularity — the hypothesis of the coarse-graining right-hand side itself — at the §4.5 data (forceBesovRegularity_of_holderHalf, forceBesovRegularity_neg_of_holderHalf), and give the printed data legs B_g, B_h ≤ C 3^{m/2}.

(M3): the ∇h leg

The ∇h leg's norm

  ‖∇h‖ = √|⨍_{□_m} ∇h|² + [∇h]_{B^t_{2,2}(□_m)}

prices against the frozen root's OWN binders. The root generator_renormalization carries, besides the seminorm binder Kh (HolderSeminormBoundOn (openCubeSet □_m) (1/2) Kh h.grad), the SUP binder

  ∀ x ∈ openCubeSet □_m, ‖h.grad x‖ ≤ KhInf

and its conclusion displays the ∇h leg as (KhInf + 3^{m/2} Kh) — the NORM, L^∞ half plus seminorm half, exactly. The mean term is priced by KhInf alone: ‖⨍_Q ∇h‖ ≤ √d · KhInf (sqrt_vecNormSq_ cubeAverageVec_le; the √d is the ambient sup-norm-versus-Euclidean conversion of vecNormSq, the standing convention, NOT a new datum). The composed display's right-hand side is the root's own bracket.

M3 is therefore NOT a statement-level item and no new binder is needed. The carrier finding stands (a Hölder SEMINORM alone does not control the mean); what that reading missed is that the root already carries the missing sup datum.

1. Hölder-1/2 data are continuous and bounded on the window

theorem Algsuperdiff.Section4.Provider.Homogenization.continuousOn_of_holderHalf {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {K : ℝ} {f : HCPolySupport.Vec d → E} (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn U (1 / 2) K f) : ContinuousOn f U

A Hölder-1/2 field is continuous on its window. The δ = (ε/(K+1))² modulus; no measurability, no completeness, no compactness is used.

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_le_of_holderHalf_of_ball {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {K R : ℝ} {f : HCPolySupport.Vec d → E} (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn U (1 / 2) K f) {x0 : HCPolySupport.Vec d} (hx0 : x0 ∈ U) (hball : U ⊆ Metric.ball x0 R) (x : HCPolySupport.Vec d) : x ∈ U → ‖f x‖ ≤ ‖f x0‖ + K * √R

A Hölder-1/2 field is bounded on a bounded window. Against any base point x₀ ∈ U inside a sup-ball of radius R.

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_le_of_holderHalf_originCube {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {m : ℤ} {K : ℝ} {f : HCPolySupport.Vec d → E} (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) (x : HCPolySupport.Vec d) : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → ‖f x‖ ≤ ‖f 0‖ + K * √(3 ^ m)

The §4.5 instance: on □_m (open realization) the base point is the origin and the sup-radius is the side length 3^m.

2. M1: the L² half of the data regularity

theorem Algsuperdiff.Section4.Provider.Homogenization.memLp_two_normalizedCubeMeasure_of_holderHalf {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {m : ℤ} {K : ℝ} {f : HCPolySupport.Vec d → E} (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) : MeasureTheory.MemLp f 2 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d m))

M1. A Hölder-1/2 datum on □_m is L² for the normalized cube measure. (normalizedCubeMeasure □_m is a probability measure; the datum is bounded on the cube by §1, and continuous there, so it is L^∞ and a fortiori L².)

3. M2: the fractional half of the data regularity

theorem Algsuperdiff.Section4.Provider.Homogenization.gagliardoCubeMeasure_eq_smul_restrict {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Gagliardo.gagliardoCubeMeasure Q = (MeasureTheory.volume (HCPolySupport.openCubeSet Q))⁻¹ • (MeasureTheory.volume.prod MeasureTheory.volume).restrict (HCPolySupport.openCubeSet Q ×ˢ HCPolySupport.openCubeSet Q)

The Gagliardo product measure on □_m, written as a scalar multiple of the plain product measure restricted to □_m × □_m. (the rewrite, at the open realization CoarseGraining's gagliardoCubeMeasure agrees with.)

theorem Algsuperdiff.Section4.Provider.Homogenization.aestronglyMeasurable_gagliardoKernel_of_holderHalf {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : HCPolySupport.TriadicCube d} {K s : ℝ} {f : HCPolySupport.Vec d → E} (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet Q) (1 / 2) K f) : MeasureTheory.AEStronglyMeasurable (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) (HCPolySupport.Gagliardo.gagliardoCubeMeasure Q)

The kernel is a.e. strongly measurable on the Gagliardo product measure. The scalar factor |z₁-z₂|^{-(s+d/2)} is GLOBALLY measurable (CoarseGraining's own idiom); only the vector factor f(z₁) - f(z₂) needs the window, and there it is continuous.

theorem Algsuperdiff.Section4.Provider.Homogenization.memWsp_of_holderHalf {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℤ} {K s : ℝ} {f : HCPolySupport.Vec d → E} (hd : 1 ≤ d) (hs0 : 0 < s) (hs : s < 1 / 2) (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) : HCPolySupport.Gagliardo.MemWsp (HCPolySupport.originCube d m) s 2 f

M2. A Hölder-1/2 datum on □_m lies in W^{s,2}(□_m) for every 0 < s < 1/2. The strict inequality s < 1/2 is load-bearing: at s = 1/2 the Gagliardo integral diverges.

4. M1 + M2: ForceBesovRegularity at the §4.5 data

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_neg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hf : Support.HolderSeminormBoundOn U alpha K f) : Support.HolderSeminormBoundOn U alpha K fun (x : HCPolySupport.Vec d) => -f x

The Hölder seminorm bound is invariant under negation.

theorem Algsuperdiff.Section4.Provider.Homogenization.forceBesovRegularity_of_holderHalf {d : ℕ} [NeZero d] {m : ℤ} {K s : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hd : 1 ≤ d) (hs0 : 0 < s) (hs : s < 1 / 2) (hK : 0 ≤ K) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K g) : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d m) s g

ForceBesovRegularity from the §4.5 Hölder normalization. This is the hypothesis the coarse-graining right-hand side itself carries, discharged at the frozen root's own data binders.

theorem Algsuperdiff.Section4.Provider.Homogenization.forceBesovRegularity_neg_of_holderHalf {d : ℕ} [NeZero d] {m : ℤ} {K s : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hd : 1 ≤ d) (hs0 : 0 < s) (hs : s < 1 / 2) (hK : 0 ≤ K) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K g) : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d m) s fun (x : HCPolySupport.Vec d) => -g x

The same for the NEGATED force, which is the forcing convention and the shape the Step-2a display consumes.

6. M3: the mean term of the ∇h leg, priced by the root's KhInf

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_cubeAverage_le_of_bound {d : ℕ} {Q : HCPolySupport.TriadicCube d} {f : HCPolySupport.Vec d → ℝ} {K : ℝ} (hf : ∀ x ∈ HCPolySupport.openCubeSet Q, |f x| ≤ K) : |HCPolySupport.cubeAverage Q f| ≤ K

Each coordinate average of a sup-bounded field is bounded by the same constant. (cubeAverage is the volume-normalized restricted Bochner integral; no integrability side condition is needed — the bound is the ‖∫‖ ≤ C · vol estimate, valid with the junk value 0 as well.)

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_vecNormSq_cubeAverageVec_le {d : ℕ} {Q : HCPolySupport.TriadicCube d} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} {K : ℝ} (hK : 0 ≤ K) (hF : ∀ x ∈ HCPolySupport.openCubeSet Q, ‖F x‖ ≤ K) : √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec Q F)) ≤ √↑d * K

M3, the mean term. ‖⨍_{□} ∇h‖ ≤ √d · K_∞ whenever ‖∇h‖ ≤ K_∞ pointwise on the cube — the root's KhInf binder verbatim. The √d is the vecNormSq-versus-supremum-norm conversion, the standing ambient convention.