HomSpineDepthGagliardoBand

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

The band factor of the single-depth Gagliardo half, and the pinned converse

What this file is for

HomSpineCzGridDepthTest reduces the depth-j dual-converse to ONE named input: a Gagliardo bound [g_j]^{p'} ≤ Cg^{p'}·(depth energy) for the depth-j slice g_j = gridDualDepthTest Q j (gridDualTestCoeff Q s p F j) (depthEnergy_rpow_le_smoothDual_of_gagliardo). HomSpineDepthFarBandSize pins the size of the band sums the input must carry. This file

• names that input in the exact BAND SHAPE the reduction produces — Cg^{p'} = C(d)·(nearBandGeometricConstant + Σ_{i<j} 3^{-i·s·p'}) (GridDepthGagliardoBandInput), with the dimensional factor C(d) a parameter, not a numeral: the reduction that would fix it is NOT proved here;
• converts the far sum into the closed 2·(s·p')⁻¹ bound uniformly in the depth (gridDepthBandFactor_le_pin, from farBand_sum_le_geom plus the elementary (1-3^{-x})⁻¹ ≤ 2·x⁻¹ of §1);
• composes with the endpoint to the depth-j converse at the EXPLICIT constant (1 + C(d)·(near + 2·x₀⁻¹))^{1/p'} on the two-sided order pin x₀ ≤ s·p' ≤ 1/2 (§3);
• discharges the consumption interface NegativeBesovGridSmoothDualConverseAtDepth at that constant and produces the SUP-FORM multiscale clause from it (§4).

The two-sided pin is necessary, not a convenience

The depth-summed grid/smooth-dual converse fixes CA BEFORE the order s, over the whole band s·p' ≤ 1/2. The far half of the single-depth Gagliardo seminorm is ≍ min(j, (s·p')⁻¹) (farBand_sum_le_geom and its lower mate), so it is unbounded as s → 0 at fixed p: no finite CA can serve the whole band through this route. Every statement below therefore carries the LOWER pin x₀ ≤ s·p' as an explicit hypothesis, and the constant is displayed as a function of x₀. At the Step-3 realization s ≍ |log γ|⁻¹ with p FIXED at 4d, x₀ ≍ |log γ|⁻¹ and the constant is ≍ |log γ|^{1/p'}.

1. The closed form of the far half at a fixed order

farBand_sum_le_geom bounds the far half by (1-3^{-x})⁻¹. On the admissible band x ≤ 1/2 that geometric factor is at most 2·x⁻¹, which is the shape the downstream constant is displayed in.

theorem Algsuperdiff.Section4.Provider.Homogenization.half_mul_le_one_sub_three_rpow_neg {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1 / 2) : x / 2 ≤ 1 - 3 ^ (-x)

The elementary lower bound on the geometric gap. On 0 < x ≤ 1/2, 1 - 3^{-x} ≥ x/2. (Proved from 1 + u ≤ exp u alone; no series.)

theorem Algsuperdiff.Section4.Provider.Homogenization.one_sub_three_rpow_neg_inv_le {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1 / 2) : (1 - 3 ^ (-x))⁻¹ ≤ 2 * x⁻¹

The geometric factor in closed form. On the admissible band 0 < x ≤ 1/2 (read x = s·p'), (1-3^{-x})⁻¹ ≤ 2·x⁻¹.

theorem Algsuperdiff.Section4.Provider.Homogenization.farBand_sum_le_two_mul_inv {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1 / 2) (j : ℕ) : ∑ i ∈ Finset.range j, 3 ^ (-x * ↑i) ≤ 2 * x⁻¹

The far half, closed and depth-uniform.

2. The band factor of the single-depth Gagliardo half

The factor the reduction of the Gagliardo double integral of a depth-j piecewise constant produces: the NEAR bands (k ≥ j, straddling measure 3^{j-k}-small against the kernel gain 3^{(k-j)·s·p'}) sum to nearBandGeometricConstant by sum_near_band_le, and the FAR bands (k < j, every pair straddling) sum to Σ_{i<j} 3^{-i·s·p'}. Only the DIMENSIONAL prefactor is left open here.

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.gridDepthBandFactor (x : ℝ) (j : ℕ) : ℝ

The band factor near + Σ_{i<j} 3^{-i x} of the single-depth Gagliardo half, at order weight x = s·p' and depth j.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.gridDepthBandFactor x j = Algsuperdiff.Section4.Provider.Homogenization.nearBandGeometricConstant + ∑ i ∈ Finset.range j, 3 ^ (-x * ↑i)

theorem Algsuperdiff.Section4.Provider.Homogenization.nearBandGeometricConstant_pos : 0 < nearBandGeometricConstant

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthBandFactor_nonneg (x : ℝ) (j : ℕ) : 0 ≤ gridDepthBandFactor x j

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthBandFactor_le {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1 / 2) (j : ℕ) : gridDepthBandFactor x j ≤ nearBandGeometricConstant + 2 * x⁻¹

The band factor is depth-uniform at a pinned order. Below x the far half saturates, so the whole factor is at most near + 2·x⁻¹, for EVERY depth.

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthBandFactor_le_pin {x₀ x : ℝ} (hx₀ : 0 < x₀) (hpin : x₀ ≤ x) (hx : x ≤ 1 / 2) (j : ℕ) : gridDepthBandFactor x j ≤ nearBandGeometricConstant + 2 * x₀⁻¹

The same bound read at a LOWER pin x₀ ≤ x: the displayed constant is monotone in the pin, so one constant serves the whole pinned band.

3. The named band input, and the pinned depth converse

def Algsuperdiff.Section4.Provider.Homogenization.GridDepthGagliardoBandInput (d : ℕ) (p : HCPolySupport.FiniteLpExponent) (Cd : ENNReal) : Prop

THE GAGLIARDO BAND INPUT.

For every cube, admissible order, field and depth: a W^{s,p'}(Q) ∩ L²(Q) carrier FOR THE DEPTH SLICE ITSELF, together with the Gagliardo bound in band form

  [g_j]_{W^{s,p'}(Q)}^{p'}  ≤  C(d)·(near + Σ_{i<j} 3^{-i·s·p'})·(depth energy).

This is exactly the hgag slot plus the carrier hGfield, with the constant spelled in the band shape HomSpineDepthFarBandSize pins two-sidedly. THIS IS A HYPOTHESIS: the reduction of the Gagliardo double integral of a depth-j piecewise constant to the band sums is NOT proved in this repository (see this file report; the missing steps are the straddling-pair measure bound at the near bands and the tail-kernel integral at the far bands).

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.gridDepthConverseConstAt (p : HCPolySupport.FiniteLpExponent) (Cd : ENNReal) (x : ℝ) (j : ℕ) : ENNReal

The DEPTH-EXACT constant delivered by the band input at order weight x and depth j: (1 + C(d)·(near + Σ_{i<j} 3^{-i x}))^{1/p'}.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.gridDepthConverseConst (p : HCPolySupport.FiniteLpExponent) (Cd : ENNReal) (x₀ : ℝ) : ENNReal

The PINNED constant: depth-uniform and order-uniform on x₀ ≤ s·p' ≤ 1/2, namely (1 + C(d)·(near + 2·x₀⁻¹))^{1/p'}.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthConverseConst_ne_top {p : HCPolySupport.FiniteLpExponent} {Cd : ENNReal} (hCd : Cd ≠ ⊤) (x₀ : ℝ) : gridDepthConverseConst p Cd x₀ ≠ ⊤

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthConverseConstAt_le {p : HCPolySupport.FiniteLpExponent} {Cd : ENNReal} {x₀ x : ℝ} (hx₀ : 0 < x₀) (hpin : x₀ ≤ x) (hx : x ≤ 1 / 2) (j : ℕ) : gridDepthConverseConstAt p Cd x j ≤ gridDepthConverseConst p Cd x₀

The depth-exact constant is below the pinned one on the pinned band.

theorem Algsuperdiff.Section4.Provider.Homogenization.depthEnergy_rpow_le_smoothDual_of_bandInput {d : ℕ} {p : HCPolySupport.FiniteLpExponent} {Cd : ENNReal} (h : GridDepthGagliardoBandInput d p Cd) (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (hband : ↑s * p.conjugate.exponent.toReal ≤ 1 / 2) (F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two) (j : ℕ) : HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovDepthEnergy Q s p F j ^ p.exponent.toReal⁻¹ ≤ gridDepthConverseConstAt p Cd (↑s * p.conjugate.exponent.toReal) j * HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm Q s p F

THE DEPTH-EXACT CONVERSE. The band input, composed with the endpoint depthEnergy_rpow_le_smoothDual_of_gagliardo, at the constant that displays the band factor of the depth actually used — no pin needed, no depth uniformity claimed.

theorem Algsuperdiff.Section4.Provider.Homogenization.depthEnergy_rpow_le_smoothDual_of_bandInput_pin {d : ℕ} {p : HCPolySupport.FiniteLpExponent} {Cd : ENNReal} {x₀ : ℝ} (hx₀ : 0 < x₀) (h : GridDepthGagliardoBandInput d p Cd) (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (hpin : x₀ ≤ ↑s * p.conjugate.exponent.toReal) (hband : ↑s * p.conjugate.exponent.toReal ≤ 1 / 2) (F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two) (j : ℕ) : HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovDepthEnergy Q s p F j ^ p.exponent.toReal⁻¹ ≤ gridDepthConverseConst p Cd x₀ * HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm Q s p F

THE PINNED DEPTH CONVERSE. On the two-sided order pin x₀ ≤ s·p' ≤ 1/2 the constant is uniform in the depth AND in the order: (1 + C(d)·(near + 2·x₀⁻¹))^{1/p'}.

4. The consumption interface, and the sup-form clause

The depth-wise converse of HomSpineCzGridDepthTest fixes one constant before the order, over the whole band s·p' ≤ 1/2; the far half is ≍ (s·p')⁻¹ there, so that shape is out of reach of this route and is NOT claimed. The pinned predicate below is what the Step-3 realization actually needs, and it discharges the interface verbatim.

def Algsuperdiff.Section4.Provider.Homogenization.DepthBandPin (p : HCPolySupport.FiniteLpExponent) (x₀ : ℝ) (s : ↑HCPolySupport.FractionalOrder) : Prop

The two-sided order pin, as the predicate the clause producer takes.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.DepthBandPin p x₀ s = (x₀ ≤ ↑s * p.conjugate.exponent.toReal ∧ ↑s * p.conjugate.exponent.toReal ≤ 1 / 2)

theorem Algsuperdiff.Section4.Provider.Homogenization.negativeBesovGridSmoothDualConverseAtDepth_of_bandInput {d : ℕ} {p : HCPolySupport.FiniteLpExponent} {Cd : ENNReal} {x₀ : ℝ} (hx₀ : 0 < x₀) (h : GridDepthGagliardoBandInput d p Cd) (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (hpin : DepthBandPin p x₀ s) (j : ℕ) : NegativeBesovGridSmoothDualConverseAtDepth Q s p j (gridDepthConverseConst p Cd x₀)

the CONSUMPTION INTERFACE, DISCHARGED at the explicit pinned constant.

theorem Algsuperdiff.Section4.Provider.Homogenization.depthConverseOn_of_bandInput {d : ℕ} {p : HCPolySupport.FiniteLpExponent} {Cd : ENNReal} {x₀ : ℝ} (hx₀ : 0 < x₀) (h : GridDepthGagliardoBandInput d p Cd) (m : ℤ) (j : ℕ) (s : ↑HCPolySupport.FractionalOrder) : DepthBandPin p x₀ s → NegativeBesovGridSmoothDualConverseAtDepth (HCPolySupport.originCube d m) s p j (gridDepthConverseConst p Cd x₀)

The producer's hypothesis, in its exact shape: the depth converse on every origin cube, every depth and every pinned order.