Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliScaleZeroRHS #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Scale-zero Caccioppoli RHS bridge helpers #
This file contains the parent-energy conversions, deterministic note-RHS translations, and scalar monotonicity helpers used by the scale-zero Caccioppoli endpoint assembly.
Audit tag #
Claim: convert deterministic note RHS quantities at scale zero into the public Chapter 3 RHS forms, including parent-energy and scalar monotonicity bridges.
Downstream target: CoarseCaccioppoliScaleZeroBridge.lean. Keep this file to
RHS translations and avoid new public *Theory surfaces.
theorem
HCPolySupport.Book.Ch03.boundary_localPatch_deterministic_note_from_public_standardExplicitBudgetSplit
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{x : Vec d}
(u : BoundaryCaccioppoliDatum Q a x)
{s t : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
:
have Csol := fullVectorPoincareCubeConstant Q;
have Calpha := coarseCaccioppoliLocalPatchBufferedAlphaBudget Q s Csol;
have Ccross := coarseCaccioppoliLocalPatchBufferedCrossBudget Q s Csol;
have Cnote :=
coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q (pointwiseCoeffFor Q a) s t
(↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross);
0 ≤ Cnote ∧ coarseCaccioppoliLocalEnergyRadiusProfile Q x
(fun (y : Vec d) => scalarVariationEnergyIntegrand (pointwiseCoeffFor Q a) u.toPointwiseAHarmonic y) (1 / 3) ≤ coarseCaccioppoliBoundaryNoteRhs Q (pointwiseCoeffFor Q a) s t Cnote
(coarseCaccioppoliHarmonicL2Sq Q (pointwiseCoeffFor Q a) u.toPointwiseAHarmonic)
theorem
HCPolySupport.Book.Ch03.boundaryCaccioppoliParentL2Sq_eq_harmonicL2Sq_pointwise
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{x : Vec d}
(u : BoundaryCaccioppoliDatum Q a x)
:
theorem
HCPolySupport.Book.Ch03.interiorCaccioppoliParentOscillationL2Sq_eq_harmonicL2Sq_pointwise_normalizeMeanZero
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn (openCubeSet Q))]
(u : CubeSolution Q a)
:
theorem
HCPolySupport.Book.Ch03.coarseCaccioppoliLocalEnergyRadiusProfile_cubeCenter_one_third_le_localizedEnergyRadiusProfile
{d : ℕ}
(Q : TriadicCube d)
{energy : Vec d → ℝ}
(henergy_nonneg : ∀ y ∈ cubeSet Q, 0 ≤ energy y)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
:
coarseCaccioppoliLocalEnergyRadiusProfile Q (cubeCenter Q) energy (1 / 3) ≤ coarseCaccioppoliLocalizedEnergyRadiusProfile Q energy (1 / 3)
theorem
HCPolySupport.Book.Ch03.interior_centered_deterministic_note_from_public_oscillation_standardExplicitBudgetSplit
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
(u : CubeSolution Q a)
{s t : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
:
have Csol := fullVectorPoincareCubeConstant Q;
have Calpha := coarseCaccioppoliBufferedAlphaBudget Q s Csol;
have Ccross := coarseCaccioppoliBufferedCrossBudget Q s Csol;
have Cnote :=
coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q (pointwiseCoeffFor Q a) s t
(↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross);
0 ≤ Cnote ∧ coarseCaccioppoliLocalizedEnergyRadiusProfile Q
(fun (y : Vec d) => scalarVariationEnergyIntegrand (pointwiseCoeffFor Q a) u.toPointwiseAHarmonic y) (1 / 3) ≤ coarseCaccioppoliInteriorNoteRhs Q (pointwiseCoeffFor Q a) s t Cnote
(interiorCaccioppoliParentOscillationL2Sq Q a u)
theorem
HCPolySupport.Book.Ch03.boundary_localPatch_standardExplicitNoteConstantSplit_le_unitExplicitBound_of_scale_zero
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffFamily d)
{s t : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hQ : Q.scale = 0)
:
have CalphaInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedAlphaBudgetUnit d s;
have CcrossInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedCrossBudgetUnit d s;
coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q (pointwiseCoeffFor Q a) s t CalphaInternal CcrossInternal ≤ caccioppoliStandardExplicitNoteBoundSplit s t CalphaInternal CcrossInternal
theorem
HCPolySupport.Book.Ch03.interior_centered_standardExplicitNoteConstantSplit_le_unitExplicitBound_of_scale_zero
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffFamily d)
{s t : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hQ : Q.scale = 0)
:
have CalphaInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedAlphaBudgetUnit d s;
have CcrossInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedCrossBudgetUnit d s;
coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q (pointwiseCoeffFor Q a) s t CalphaInternal CcrossInternal ≤ caccioppoliStandardExplicitNoteBoundSplit s t CalphaInternal CcrossInternal
theorem
HCPolySupport.Book.Ch03.deterministic_boundaryNoteRhs_pointwiseCoeffFor_le_publicPrefactor_dim_sq_mul
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{s t C uL2Sq : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hC : 0 ≤ C)
(hQscale : Q.scale = 0)
(hu : 0 ≤ uL2Sq)
:
coarseCaccioppoliBoundaryNoteRhs Q (pointwiseCoeffFor Q a) s t C uL2Sq ≤ caccioppoliPrefactor (↑d ^ 2 * C) Q a s t * uL2Sq
theorem
HCPolySupport.Book.Ch03.deterministic_boundaryNoteRhs_pointwiseCoeffFor_le_publicRHS_dim_sq_mul_of_scale_zero
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{x : Vec d}
(u : BoundaryCaccioppoliDatum Q a x)
{s t C : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hC : 0 ≤ C)
(hQscale : Q.scale = 0)
:
coarseCaccioppoliBoundaryNoteRhs Q (pointwiseCoeffFor Q a) s t C (boundaryCaccioppoliParentL2Sq u) ≤ boundaryCaccioppoliRHS (↑d ^ 2 * C) s t u
theorem
HCPolySupport.Book.Ch03.deterministic_interiorNoteRhs_pointwiseCoeffFor_le_publicRHS_dim_sq_mul_of_scale_zero
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
(u : CubeSolution Q a)
{s t C : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hC : 0 ≤ C)
(hQscale : Q.scale = 0)
:
coarseCaccioppoliInteriorNoteRhs Q (pointwiseCoeffFor Q a) s t C (interiorCaccioppoliParentOscillationL2Sq Q a u) ≤ interiorCaccioppoliRHS (↑d ^ 2 * C) Q a s t u