The space-time-agnostic integration-by-parts core that the weak-divergence, weak-momentum,
and local-energy-inequality clauses of CKN.IsSuitableWeakSolution all need to move a spatial or
temporal derivative from a classical (ContDiffOn, not globally ContDiff) field onto a smooth
compactly-supported test function.
theorem
CIV.integrableOn_mul_of_continuousOn_of_tsupport_subset
{E : Type}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
[T2Space E]
{μ : MeasureTheory.Measure E}
[μ.IsAddHaarMeasure]
{S K : Set E}
{g ρ : E → ℝ}
(hK : IsCompact K)
(hKS : K ⊆ S)
(hg : ContinuousOn g S)
(hρ : Continuous ρ)
(hsupp : tsupport ρ ⊆ K)
:
MeasureTheory.Integrable (fun (x : E) => g x * ρ x) μ
theorem
CIV.integrable_mul_fderiv_of_continuousOn
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
[T2Space E]
{μ : MeasureTheory.Measure E}
[μ.IsAddHaarMeasure]
{S K : Set E}
{g ψ : E → ℝ}
{v : E}
(hK : IsCompact K)
(hKS : K ⊆ S)
(hg : ContinuousOn g S)
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hsupp : tsupport ψ ⊆ K)
:
MeasureTheory.Integrable (fun (x : E) => g x * (fderiv ℝ ψ x) v) μ
theorem
CIV.integral_mul_fderiv_eq_neg_fderiv_mul_of_continuousOn
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[OpensMeasurableSpace E]
[T2Space E]
[FiniteDimensional ℝ E]
{μ : MeasureTheory.Measure E}
[μ.IsAddHaarMeasure]
{S K : Set E}
{h ψ : E → ℝ}
{v : E}
(hSopen : IsOpen S)
(hK : IsCompact K)
(hKS : K ⊆ S)
(hh : ContDiffOn ℝ (↑⊤) h S)
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hsupp : tsupport ψ ⊆ K)
: