OAI/Analysis/AffineBernstein/BaseLogIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.flatCofactorTrace_eq_det_mul line 17
2. lemma OAI.AffineBernstein.flatCofactorPair_eq_det_mul line 23
3. lemma OAI.AffineBernstein.flatCofactorTrace_log line 32
4. theorem OAI.AffineBernstein.integral_base_log_identity line 52

   Source comment

   Pointwise logarithmic Hessian identity plus genuine base integration by parts gives the source p-identity. Its density is exactly `W detB/H`.

   theorem integral_base_log_identity {D : Set E} (hD : IsOpen D) {H F σ : E → ℝ}
       (hH : ContDiffOn ℝ ∞ H D) (hF : ContDiffOn ℝ ∞ F D)
       (hpos : ∀ x ∈ D, 0 < H x) (v : ι → E)
       (hd : ∀ x ∈ D, (-flatBlockHessian H v x).det ≠ 0)
       (hσ : ContDiff ℝ ∞ σ) (hc : HasCompactSupport σ) (hσD : tsupport σ ⊆ D)
       (n c : ℝ) :
       let K := fun x => -H x
   …

   Mentions: OAI.AffineBernstein.flatBlockHessian