Coarse-graining support: Support.Book.Ch01.Theorems.HodgeProjectionL2

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Ch1 Hilbert L² Hodge projection input

This file proves the Hilbert-space core of the unit Dirichlet Hodge projection estimate. The concrete negative-Besov theorem still needs boundedness of the same projection in the Besov scale; the orthogonality and energy estimate here are unconditional.

theorem HCPolySupport.Book.Ch01.IsPotentialZeroTraceOn.memVectorL2 {d : ℕ} {U : Set (Vec d)} {w : Vec d → Vec d} (hw : IsPotentialZeroTraceOn U w) : MemVectorL2 U w

A zero-trace potential field has the L² membership supplied by its H¹₀ primitive.

theorem HCPolySupport.Book.Ch01.inner_toHilbertVectorL2OfVecField_eq_zero_of_isPotentialZeroTraceOn_of_isSolenoidalOn {d : ℕ} (Q : TriadicCube d) {w z : Vec d → Vec d} (hwMem : MemVectorL2 (cubeSet Q) w) (hzMem : MemVectorL2 (cubeSet Q) z) (hw : IsPotentialZeroTraceOn (cubeSet Q) w) (hz : IsSolenoidalOn (cubeSet Q) z) : inner ℝ (toHilbertVectorL2OfVecField hwMem) (toHilbertVectorL2OfVecField hzMem) = 0

Zero-trace potential fields are L²-orthogonal to solenoidal fields.

theorem HCPolySupport.Book.Ch01.exists_h10Gradient_firstVariation_eq_negativeForcing {d : ℕ} {U : Set (Vec d)} {w F : Vec d → Vec d} (hF : MemVectorL2 U F) (hw : IsPotentialZeroTraceOn U w) (hsol : IsSolenoidalOn U fun (x : Vec d) => w x + F x) : ∃ (u : H10Function U), u.grad = w ∧ ∀ (φ : H10Function U), ∫ (x : Vec d) in U, vecDot (u.grad x) (φ.grad x) = -∫ (x : Vec d) in U, vecDot (F x) (φ.grad x)

The zero-trace primitive of a Hodge potential component solves the Dirichlet variational problem with right-hand side -F.

This is the PDE identity behind the unit Hodge projection: if w is zero-trace potential and w + F is solenoidal, then the primitive of w tests against every zero-trace gradient as -F.

theorem HCPolySupport.Book.Ch01.unitHodgeProjectionL2Estimate {d : ℕ} (Q : TriadicCube d) (w F : Vec d → Vec d) (hF : MemVectorL2 (cubeSet Q) F) (hw : IsPotentialZeroTraceOn (cubeSet Q) w) (hsol : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => w x + F x) : ‖toHilbertVectorL2OfVecField ⋯‖ + ‖toHilbertVectorL2OfVecField ⋯‖ ≤ 2 * ‖toHilbertVectorL2OfVecField hF‖

Unit Dirichlet Hodge projection estimate in the Hilbert L² norm.

If w is the zero-trace potential component and w + F is solenoidal, both components are controlled by the forcing field F.