Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.WeakTesting #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.integrableOn_vecDot_harmonicFlux_harmonicFunction_scalarCutoffGradientField
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
:
MeasureTheory.IntegrableOn
(fun (x : Vec d) => vecDot (matVecMul (a x) (w.toH1.grad x)) (w.toH1.toFun x • scalarCutoffGradientField η x))
(cubeSet Q) MeasureTheory.volume
The harmonic flux tested against u ∇η is integrable on the closed cube.
The weak-testing identity below already proves this internally on the open cube; this lemma exposes the integrability input needed by descendant summation.
theorem
HCPolySupport.setIntegral_scalarVariationEnergy_eq_neg_fluxCutoffPairing_of_memH10
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
(hw_memH10 : MemH10 (openCubeSet Q) fun (x : Vec d) => η x * w.toH1.toFun x)
:
theorem
HCPolySupport.setIntegral_scalarVariationEnergy_eq_neg_fluxCutoffPairing
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
(hη_sub : tsupport η ⊆ openCubeSet Q)
:
theorem
HCPolySupport.setIntegral_scalarVariationEnergy_eq_neg_fluxCutoffPairing_of_aHarmonicFunction
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{V : Set (Vec d)}
(hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) V w.toH1.toFun)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
(hη_sub : tsupport η ⊆ V)
:
theorem
HCPolySupport.cubeAverage_scalarVariationEnergy_eq_neg_fluxCutoffPairing
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
(hη_sub : tsupport η ⊆ openCubeSet Q)
:
(cubeAverage Q fun (x : Vec d) => η x * scalarVariationEnergyIntegrand a w x) = -cubeAverage Q fun (x : Vec d) =>
vecDot (matVecMul (a x) (w.toH1.grad x)) (w.toH1.toFun x • scalarCutoffGradientField η x)
theorem
HCPolySupport.cubeAverage_scalarVariationEnergy_eq_neg_fluxCutoffPairing_of_aHarmonicFunction
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{V : Set (Vec d)}
(hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) V w.toH1.toFun)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
(hη_sub : tsupport η ⊆ V)
:
(cubeAverage Q fun (x : Vec d) => η x * scalarVariationEnergyIntegrand a w x) = -cubeAverage Q fun (x : Vec d) =>
vecDot (matVecMul (a x) (w.toH1.grad x)) (w.toH1.toFun x • scalarCutoffGradientField η x)
theorem
HCPolySupport.le_abs_cubeAverage_vectorDot_flux_scalarCutoffGradientField
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam F : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
(hη_sub : tsupport η ⊆ openCubeSet Q)
(hlower : F ≤ cubeAverage Q fun (x : Vec d) => η x * scalarVariationEnergyIntegrand a w x)
:
theorem
HCPolySupport.le_abs_cubeAverage_vectorDot_flux_scalarCutoffGradientField_of_aHarmonicFunction
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{lam Lam F : ℝ}
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
{V : Set (Vec d)}
(hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) V w.toH1.toFun)
{η : Vec d → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hη_compact : HasCompactSupport η)
(hη_sub : tsupport η ⊆ V)
(hlower : F ≤ cubeAverage Q fun (x : Vec d) => η x * scalarVariationEnergyIntegrand a w x)
: