CubeSchauderFreezingResidue #

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

Cube Schauder: the freezing residue in coordinate `L²` form #

The freezing step of CubeSchauderFreezing delivers its harmonic-approximation error as a Dirichlet energy, ∫_□ |∇w|². The consumers of that error — the zero-trace Poincaré inequality and the development's one-step excess contraction — both take the coordinate sum Σᵢ ‖∂ᵢ w‖_{L²(□)} instead. This module supplies the missing dictionary and reads the freezing gain off in that shape.

The dictionary is Cauchy--Schwarz on Fin d applied to the vector of coordinate L² norms:

  Σᵢ ‖∂ᵢ w‖_{L²(U)} ≤ √( d · ∫_U |∇w|² ) .

Combined with the freezing bound ∫_□ |∇w|² ≤ d · KG² · 3^j · |□_j| of exists_frozenHarmonicReplacement_openCubeSet this gives

  Σᵢ ‖∂ᵢ w‖_{L²(□_j)} ≤ d · KG · √( 3^j · |□_j| ) ,

i.e. the freezing gain (3^j)^{1/2}·[G]_{C^{0,1/2}} in the exact slot shape of the proved Dirichlet-Poincaré and one-step machinery.

Main results #

sum_toReal_eLpNorm_coord_le — the Cauchy--Schwarz dictionary.
sum_toReal_eLpNorm_grad_le_of_dirichletEnergy_le — its H¹ instance.
exists_frozenHarmonicReplacement_coordL2 — the freezing step on an origin cube, with the residue delivered as Σᵢ ‖∂ᵢ w‖_{L²} at the explicit constant d · KG · √(3^j · (3^j)^d).

References #

Armstrong--Kuusi, Elliptic Regularity (ellipticregularity.tex), the harmonic-approximation display e.harmapprox.Sch.onealpha.
ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.

1. The Cauchy--Schwarz dictionary #

source

theorem Algsuperdiff.Section4.Provider.Schauder.sum_toReal_eLpNorm_coord_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => F x i) 2 (MeasureTheory.volume.restrict U)) :

∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => F x i) 2 (MeasureTheory.volume.restrict U)).toReal ≤ √(↑d * ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecNormSq (F x))

The coordinate-sum dictionary.

The sum of the coordinate L² norms of a vector field is at most √d times its Dirichlet-type L² norm. This is Cauchy--Schwarz on Fin d against the vector of ones.

source