Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliRHS.EnergySplit

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

Coarse Caccioppoli with RHS Energy Split

This file is split mechanically out of CoarseCaccioppoliRHS.lean.

Audit tag

Claim: split forced boundary Caccioppoli energy into the homogeneous part, zero-trace corrector part, and cross terms using the public coefficient representative.

Downstream target: CoarseCaccioppoliRHS/Prefactors.lean and CoarseCaccioppoliRHS/FinalBounds.lean. This file should contain energy identities and inequalities only.

theorem HCPolySupport.Book.Ch03.localizedCoeffEnergyValue_eq_volumeAverage_publicCoeffField_of_subset_openCubeSet {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {V : Set (Vec d)} (hV : V ⊆ openCubeSet Q) (u : H1Function (Ch02.cubeDomain Q).carrier) : localizedCoeffEnergyValue V (a.coeffOn Q) u = volumeAverage V (coefficientEnergyDensity (publicCoeffField Q a) u.grad)

On subsets of the open cube, public localized energy can be evaluated using the pointwise deterministic coefficient representative.

theorem HCPolySupport.Book.Ch03.volumeAverage_coefficientEnergyDensity_le_two_mul_add_of_ae_eq_add {d : ℕ} {V : Set (Vec d)} {A : CoeffField d} {lam Lam : ℝ} {F G H : Vec d → Vec d} (hEll : IsEllipticFieldOn lam Lam V A) (hF : MemVectorL2 V F) (hG : MemVectorL2 V G) (hH : MemVectorL2 V H) (hFGH : F =ᵐ[volumeMeasureOn V] fun (y : Vec d) => G y + H y) : volumeAverage V (coefficientEnergyDensity A F) ≤ 2 * volumeAverage V (coefficientEnergyDensity A G) + 2 * volumeAverage V (coefficientEnergyDensity A H)

Coefficient-energy triangle inequality for a decomposition F = G + H over an arbitrary measurable set.

theorem HCPolySupport.Book.Ch03.normalizedSetAverage_caccioppoliCoreSet_le_eighteen_pow_mul_cubeAverage {d : ℕ} (Q : TriadicCube d) {x : Vec d} {energy : Vec d → ℝ} (hx : x ∈ openCubeSet Q) (henergy_nonneg : ∀ y ∈ cubeSet Q, 0 ≤ energy y) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : normalizedSetAverage (caccioppoliCoreSet Q x) energy ≤ 18 ^ d * cubeAverage Q energy

A core average is controlled by the parent cube average with the dimension-only volume ratio 18^d.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrector_coreEnergy_le_eighteen_pow_mul_parentEnergy {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hx : x ∈ openCubeSet Q) : localizedCoeffEnergyValue (caccioppoliCoreSet Q x) (a.coeffOn Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toH1Function ≤ 18 ^ d * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (y : Vec d) => ρ.toH10.grad y)

The zero-trace corrector's localized core energy is controlled by its parent cube coefficient energy with only the geometric 18^d loss.

theorem HCPolySupport.Book.Ch03.zeroDirichletEnergyWithRHSRHS_nonneg {d : ℕ} {C : ℝ} (hC_nonneg : 0 ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (ht : 0 < t) (hg : ForceBesovRegularity Q (2 * t) g) : 0 ≤ zeroDirichletEnergyWithRHSRHS C Q a t g

The public zero-Dirichlet RHS is nonnegative under the force regularity hypothesis.

theorem HCPolySupport.Book.Ch03.corrector_parentEnergy_le_zeroDirichletRHS_squared {d : ℕ} [NeZero d] {C : ℝ} (hC_nonneg : 0 ≤ C) (hC_zero : √(250 + 2 * √15000 * √2) * (↑d * Real.rpow 3 (↑d + 1)) ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (ht : 0 < t) (ht_lt : t < 1 / 2) (hg : ForceBesovRegularity Q (2 * t) g) : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => ρ.toH10.grad x) ≤ zeroDirichletEnergyWithRHSRHS (↑d * C) Q a t g ^ 2

Squared form of the zero-trace corrector energy estimate, tuned to the t-notation used by the boundary Caccioppoli RHS theorem.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrector_coreEnergy_le_eighteen_pow_mul_zeroDirichletEnergyWithRHSRHS_sq {d : ℕ} [NeZero d] {C : ℝ} (hC_nonneg : 0 ≤ C) (hC_zero : √(250 + 2 * √15000 * √2) * (↑d * Real.rpow 3 (↑d + 1)) ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {x : Vec d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (ht : 0 < t) (ht_lt : t < 1 / 2) (hx : x ∈ openCubeSet Q) (hg : ForceBesovRegularity Q (2 * t) g) : localizedCoeffEnergyValue (caccioppoliCoreSet Q x) (a.coeffOn Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toH1Function ≤ 18 ^ d * zeroDirichletEnergyWithRHSRHS (↑d * C) Q a t g ^ 2

The localized corrector core is controlled directly by the square of the public zero-Dirichlet RHS, with only the geometric 18^d loss.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCoreEnergy_le_two_mul_remainder_add_corrector {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) : boundaryForcedCaccioppoliCoreEnergy u ≤ 2 * boundaryCaccioppoliCoreEnergy (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem) + 2 * localizedCoeffEnergyValue (caccioppoliCoreSet Q x) (a.coeffOn Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toH1Function

Localized core-energy split for the manuscript decomposition u = w + ρ.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainder_parentL2_le_two_mul_forced_add_corrector {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) : boundaryCaccioppoliParentL2Sq (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem) ≤ 2 * boundaryForcedCaccioppoliParentL2Sq u + 2 * normalizedL2SqOnSet (openCubeSet Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toFun

Parent L² split for the manuscript decomposition w = u - ρ.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainder_coreEnergy_le_homogeneousRHS {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hx : x ∈ openCubeSet Q) : ∃ (C : ℝ), 0 < C ∧ boundaryCaccioppoliCoreEnergy (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem) ≤ boundaryCaccioppoliRHS C s t (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem)

Apply the proved homogeneous boundary Caccioppoli theorem to the harmonic remainder produced from a forced datum.