CubeSchauderPoincare

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

Cube Schauder: the Dirichlet Poincaré on an inscribed window

  ‖σ‖_{L²(W)} ≤ C(d) · 3^n · Σᵢ ‖∂ᵢσ‖_{L²(W)} ,   σ ∈ H¹₀(W) ,

for every window W inscribed in a translated triadic cube c + □_n.

ExcessDecay.BoundarySplit.eLpNorm_le_dirichletCubePoincare proves the special case W = □_n, but that module's import cone reaches Algsuperdiff.Frozen, which the Schauder cone must not. The statement is therefore re-proved here, from the two genuinely needed leaves (BoundaryPoincareCore's zero-set core and BoundaryTraceMeasure's zero extension and slab covering, both Frozen-free), and at the same time generalized off the cube: the truncated windows (x + □_n) ∩ □_m of the §4 lane are inscribed in x + □_n but are not cubes, and it is those windows the composition needs.

The mechanism is unchanged: the zero extension of σ to the parent cube c + □_{n+1} vanishes on the upper slab {yᵢ ≥ cᵢ + ½·3^n}, which carries at least a third of the parent (three translates of the slab cover it), so the zero-set Poincaré inequality applies at the parent's scale 3^{n+1}.

Main results

• schauderDirichletPoincareConst — the constant 3(1+√3)·C_meanzero(d).
• eLpNorm_le_schauderDirichletPoincare — the inequality above.

References

• ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.

1. The constant

noncomputable def Algsuperdiff.Section4.Provider.Schauder.schauderDirichletPoincareConst (d : ℕ) : ℝ

The coefficient-free constant of the inscribed-window Dirichlet Poincaré inequality: 3(1 + √3) times the d-only mean-zero constant of the unit corner cube.

Equations

• Algsuperdiff.Section4.Provider.Schauder.schauderDirichletPoincareConst d = (1 + √3) * (HCPolySupport.unitMeanZeroPoincareConst d * 3)

theorem Algsuperdiff.Section4.Provider.Schauder.schauderDirichletPoincareConst_nonneg (d : ℕ) : 0 ≤ schauderDirichletPoincareConst d

2. The parent cube and its upper slab

theorem Algsuperdiff.Section4.Provider.Schauder.volume_parentCube_le_three_mul_upperSlab {d : ℕ} (c : HCPolySupport.Vec d) (n : ℤ) (i : Fin d) : MeasureTheory.volume (HCPolySupport.axisCube (fun (j : Fin d) => c j - 1 / 2 * 3 ^ (n + 1)) (3 ^ (n + 1))) ≤ 3 * MeasureTheory.volume (HCPolySupport.axisCube (fun (j : Fin d) => c j - 1 / 2 * 3 ^ (n + 1)) (3 ^ (n + 1)) ∩ {y : HCPolySupport.Vec d | c i + 1 / 2 * 3 ^ n ≤ y i})

The parent's upper slab carries a third of the parent.

The level cᵢ + ½·3^n — the upper face of the inscribing cube c + □_n — cuts the parent cube c + □_{n+1} so that the part above it is at least a third of the parent. This is volume_le_three_mul_slab at lo = cᵢ - ½·3^{n+1}, hi = cᵢ + ½·3^{n+1}, a = cᵢ + ½·3^n, where a - 2(hi - a) = lo exactly.

3. The Dirichlet Poincaré on an inscribed window

theorem Algsuperdiff.Section4.Provider.Schauder.eLpNorm_le_schauderDirichletPoincare {d : ℕ} [NeZero d] {W : Set (HCPolySupport.Vec d)} (hWmeas : MeasurableSet W) (c : HCPolySupport.Vec d) (n : ℤ) (hWsub : ∀ y ∈ W, ∀ (j : Fin d), c j - 1 / 2 * 3 ^ n < y j ∧ y j < c j + 1 / 2 * 3 ^ n) (sigma : HCPolySupport.H10Function W) : (MeasureTheory.eLpNorm sigma.toFun 2 (MeasureTheory.volume.restrict W)).toReal ≤ schauderDirichletPoincareConst d * 3 ^ n * ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => sigma.grad y i) 2 (MeasureTheory.volume.restrict W)).toReal

The Dirichlet Poincaré inequality on an inscribed window.

An H¹₀(W) datum on a measurable window W ⊆ c + □_n obeys the un-subtracted L² Poincaré inequality at the inscribing cube's scale 3^n, with a constant depending on d alone.

This is the converter of the §4.5 Campanato composition: the freezing step of CubeSchauderFreezing delivers Σᵢ ‖∂ᵢw‖_{L²}, and the one-step contraction consumes ‖u − v‖_{L²}.