HomSpineDepthBandInput

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

THE GAGLIARDO BAND INPUT, DISCHARGED — and the unconditional sup clause

What this file is for

HomSpineDepthGagliardoBand reduced the sup-form multiscale clause to ONE named input, GridDepthGagliardoBandInput d p Cd. This file discharges it at the explicit numeral

  Cd = gridDepthGagliardoConst d p = 2^{p'} · 2^{d+3} · (d+1) · 3^d.

Three pieces.

• lintegral_normalized_enorm_gridDualTestCoeff_le — the FLAT half in the exact form the reduction needs: ⨍_Q ‖g_j‖^{p'} ≤ (cell side)^{s·p'}·(depth energy), the same conjugacy bookkeeping (p-1)p' = p, p·p' = p+p' as HomSpineCzGridDepthTest.weight_mul_flat_rpow_le_depthEnergy but keeping the 3^{-s·j·p'} that display discards — it is exactly the cell-side weight the band reduction produces.
• gridDepthGagliardoBandInput_holds — the input, carrier and all: the W^{s,p'} ∩ L² bundle for the depth slice (its Gagliardo finiteness IS the reduction, its L² half is the finite indicator sum), and the band bound. Together they leave the SUP-FORM MULTISCALE CLAUSE with NO named input: HomSpineDepthGagliardoBand's producer runs at Cd = gridDepthGagliardoConst d p, so at CA = (1 + Cd·(near + 2·x₀⁻¹))^{1/p'} on the two-sided order pin x₀ ≤ s·p' ≤ 1/2.

1. The L^q membership of a depth slice

theorem Algsuperdiff.Section4.Provider.Homogenization.ofVec_gridDualDepthTest_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (x : HCPolySupport.Vec d) : HCPolySupport.HilbertVec.ofVec (gridDualDepthTest Q j v x) = ∑ R ∈ HCPolySupport.descendantsAtDepth Q j, (HCPolySupport.cubeSet R).indicator (fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (v R)) x

The depth slice, as a finite sum of indicators in the Hilbert realization.

theorem Algsuperdiff.Section4.Provider.Homogenization.memLp_ofVec_gridDualDepthTest {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (q : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (gridDualDepthTest Q j v x)) q (HCPolySupport.normalizedCubeMeasure Q)

A depth slice belongs to every L^q(Q): it is a finite sum of constants times indicators of measurable sets, on a finite measure.

2. The flat half, with the cell-side weight kept

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_normalized_enorm_gridDualTestCoeff_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two) (j : ℕ) : ∫⁻ (x : HCPolySupport.Vec d), ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j (gridDualTestCoeff Q (↑s) p.exponent.toReal F.toField j) x)‖ₑ ^ p.conjugate.exponent.toReal ∂HCPolySupport.normalizedCubeMeasure Q ≤ ENNReal.ofReal ((HCPolySupport.cubeScaleFactor Q / 3 ^ j) ^ (↑s * p.conjugate.exponent.toReal)) * HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovDepthEnergy Q s p F j

THE FLAT HALF. The normalized L^{p'} mass of the depth slice is below (cell side)^{s·p'} times the depth energy. (HomSpineCzGridDepthTest's weight_mul_flat_rpow_le_depthEnergy throws this weight away against the scale factor of the full norm; the band reduction needs it, because the band factor is displayed relative to the CELL scale, not the cube scale.)

3. The band input, discharged

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoConst (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : ENNReal

THE DIMENSIONAL GAGLIARDO BAND CONSTANT, pinned: 2^{p'}·2^{d+3}·(d+1)·3^d. The 2^{p'} is the crude increment splitting (ennreal_add_rpow_le) and is bounded only on a bounded range of p' — on the repository's band p ≥ 2 it is at most 4.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoConst d p = ENNReal.ofReal (2 ^ p.conjugate.exponent.toReal * (2 ^ (d + 3) * (↑d + 1) * 3 ^ d))

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoConst_ne_top (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : gridDepthGagliardoConst d p ≠ ⊤

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoBandInput_holds (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : GridDepthGagliardoBandInput d p (gridDepthGagliardoConst d p)

THE BAND INPUT, DISCHARGED. HomSpineDepthGagliardoBand's one named input holds, at the explicit numeral gridDepthGagliardoConst d p.