OAI/Analysis/AffineBernstein/BaseWeightedIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.integrable_local_mul_test line 16
2. lemma OAI.AffineBernstein.integrable_local_mul_dirDeriv_test line 25
3. theorem OAI.AffineBernstein.integral_flatCofactor_trace line 37

   Source comment

   Base cofactor integration by parts. Only smoothness near the compact test support is needed; no boundary regularity or global coefficient extension is assumed.

   theorem integral_flatCofactor_trace {f β g σ : E → ℝ} (v : ι → E)
       (hσ : ContDiff ℝ ∞ σ) (hc : HasCompactSupport σ)
       (hf : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ f x)
       (hβ : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ β x)
       (hg : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ g x) :
       (∫ x, (β x*flatCofactorTrace f v g x+flatCofactorPair f v β g x)*σ x ∂μ) =
         -(∫ x, β x*flatCofactorPair f v σ g x ∂μ) := by
   …

   Mentions: OAI.AffineBernstein.flatCofactorTrace, OAI.AffineBernstein.flatCofactorPair