Coarse-graining support: Support.Book.Ch03.Theorems.EnergyRHS.DirichletSplit

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

Energy RHS: Dirichlet splitting

theorem HCPolySupport.Book.Ch03.dirichletForcedSolutionEnergyNorm_le_sqrt_two_mul_zeroTraceDifference_add_boundary {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) : dirichletForcedSolutionEnergyNorm Q a v ≤ √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => v.zeroTraceDifferenceH10CubeSet.grad x) + 2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) (dirichletBoundaryGradientField v)))

Dirichlet forced-solution energy reduced to the chosen zero-trace correction and the boundary-gradient energy. This is the square-root form of the public v = (v - h) + h energy split.

theorem HCPolySupport.Book.Ch03.cubeAverage_coefficientEnergyDensity_le_two_mul_add_of_ae_eq_add {d : ℕ} {Q : TriadicCube d} {A : CoeffField d} {lam Lam : ℝ} {F G H : Vec d → Vec d} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) A) (hF : MemVectorL2 (cubeSet Q) F) (hG : MemVectorL2 (cubeSet Q) G) (hH : MemVectorL2 (cubeSet Q) H) (hFGH : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] fun (x : Vec d) => G x + H x) : cubeAverage Q (coefficientEnergyDensity A F) ≤ 2 * cubeAverage Q (coefficientEnergyDensity A G) + 2 * cubeAverage Q (coefficientEnergyDensity A H)

Coefficient-energy triangle inequality for a decomposition F = G + H on the cube. This is the reusable analytic split behind the Dirichlet proof route v = v₀ + \widetilde h.

theorem HCPolySupport.Book.Ch03.dirichletForcedSolutionEnergyNorm_le_sqrt_two_mul_zeroTraceCorrector_add_harmonicRemainder {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hgrad : v.toH1.grad =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] fun (x : Vec d) => ρ.toH10.grad x + w.toH1.grad x) : dirichletForcedSolutionEnergyNorm Q a v ≤ √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => ρ.toH10.grad x)) + √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x))

Dirichlet forced-solution energy split along the manuscript decomposition v = v₀ + \widetilde h, where v₀ is a zero-Dirichlet corrector and \widetilde h is the homogeneous boundary-data remainder.

theorem HCPolySupport.Book.Ch03.dirichletForcedSolutionEnergyNorm_le_of_zeroTraceCorrector {d : ℕ} [NeZero d] {C : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hgrad : v.toH1.grad =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] fun (x : Vec d) => ρ.toH10.grad x + w.toH1.grad x) (hzero : √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => ρ.toH10.grad x)) ≤ C * s.rpow (-(3 / 2)) * poincareLowerEllipticityFactor Q a (s / 2) (Ch02.MultiscaleExponent.finite 2) * scaleNormalizedPositiveBesovVectorSeminormTwo Q s g) (hharmonic : √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x)) ≤ C * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)) : dirichletForcedSolutionEnergyNorm Q a v ≤ dirichletEnergyWithRHSRHS C Q a s g v

Manuscript-route assembly for the public Dirichlet estimate: after choosing the zero-Dirichlet forced corrector and the homogeneous boundary remainder, the two square-root bounds imply the displayed RHS.