OAI/Analysis/AffineBernstein/BaseExponentialIBP.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.dirDeriv_exp_linear_combination line 14
2. lemma OAI.AffineBernstein.flatCofactorPair_exp line 25
3. lemma OAI.AffineBernstein.flatCofactorPair_test_square line 38
4. theorem OAI.AffineBernstein.integral_flatCofactor_exp_square line 53

   Source comment

   Base identity for the exact exponential weight and a squared compact test. It is valid without global smooth extensions of the support function.

   theorem integral_flatCofactor_exp_square {f P F g σ : E → ℝ} (v : ι → E)
       (hσ : ContDiff ℝ ∞ σ) (hc : HasCompactSupport σ)
       (hf : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ f x)
       (hP : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ P x)
       (hF : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ F x)
       (hg : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ g x) (a b : ℝ) :
       (∫ x, Real.exp (a*P x+b*F x)*σ x^2 *
         (flatCofactorTrace f v g x+a*flatCofactorPair f v P g x+b*flatCofactorPair f v F g x) ∂μ) =
         -2*(∫ x, Real.exp (a*P x+b*F x)*σ x*flatCofactorPair f v σ g x ∂μ) := by
   …

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