AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedBochner

- Actual weighted Bochner identity, all compact-test integrability facts, and its curvature-energy consequence. This does not establish Poincare.

theorem integrated_bochner_identity (W f : E → ℝ) (hW : ContDiff ℝ 2 W)
    (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f) :
    let L := fun x => Laplacian.laplacian f x - inner ℝ (gradient W x) (gradient f x)
    let H := fun x => ∑ i, ‖gradient (fun z => fderiv ℝ f z ((stdOrthonormalBasis ℝ E) i)) x‖^2
    let C := fun x => fderiv ℝ (fderiv ℝ W) x (gradient f x) (gradient f x)
    Integrable (fun x => Real.exp (-W x) * (L x)^2) ∧
    Integrable (fun x => Real.exp (-W x) * ‖gradient f x‖^2) ∧
    Integrable (fun x => Real.exp (-W x) * H x) ∧
    Integrable (fun x => Real.exp (-W x) * C x) ∧
    (∫ x, Real.exp (-W x) * (L x)^2) =
      (∫ x, Real.exp (-W x) * H x) + ∫ x, Real.exp (-W x) * C x ∧
    ∀ m : ℝ, (∀ x v, m * ‖v‖^2 ≤ fderiv ℝ (fderiv ℝ W) x v v) →
      m * (∫ x, Real.exp (-W x) * ‖gradient f x‖^2) ≤ ∫ x, Real.exp (-W x) * (L x)^2 := by
  have weighted_directional_ibp (W g h : E → ℝ) (hW : ContDiff ℝ 1 W) (hg : ContDiff ℝ 1 g)
      (hh : ContDiff ℝ 2 h) (hc : HasCompactSupport h) (v : E) :
      (∫ x, (Real.exp (-W x) * g x) *
        fderiv ℝ (fun z => fderiv ℝ h z v) x v) =
      - ∫ x, Real.exp (-W x) *
        (fderiv ℝ g x v - g x * fderiv ℝ W x v) * fderiv ℝ h x v := by
    let F := fun x => Real.exp (-W x) * g x
    let H := fun x => fderiv ℝ h x v
    have hF : ContDiff ℝ 1 F := hW.neg.exp.mul hg
    have hH : ContDiff ℝ 1 H :=
      (hh.fderiv_right (m := 1) (by norm_num)).clm_apply contDiff_const
    have hHc : HasCompactSupport H := by
      refine HasCompactSupport.of_support_subset_isCompact hc.isCompact ?_
      intro x hx
      by_contra hnot
      exact hx (by simp [H, fderiv_of_notMem_tsupport ℝ hnot])
    have hDHc : HasCompactSupport (fun x => fderiv ℝ H x v) := by
      refine HasCompactSupport.of_support_subset_isCompact hHc.isCompact ?_
      intro x hx
      by_contra hnot
      exact hx (by simp [fderiv_of_notMem_tsupport ℝ hnot])
    have hDF : Continuous (fun x => fderiv ℝ F x v) :=
      (hF.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
    have hDH : Continuous (fun x => fderiv ℝ H x v) :=
      (hH.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
    have h1 : Integrable (fun x => fderiv ℝ F x v * H x) :=
      (hDF.mul hH.continuous).integrable_of_hasCompactSupport hHc.mul_left
    have h2 : Integrable (fun x => F x * fderiv ℝ H x v) :=
      (hF.continuous.mul hDH).integrable_of_hasCompactSupport hDHc.mul_left
    have h3 : Integrable (fun x => F x * H x) :=
      (hF.continuous.mul hH.continuous).integrable_of_hasCompactSupport hHc.mul_left
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedBochner.lean:34published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.