AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradient

No declaration docstring.

theorem compact_gradient_closable (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∃ D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ,
      Dense (D.domain : Set (Lp ℝ 2 μ)) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
      ∀ (u : Lp ℝ 2 μ) (v : Lp E 2 μ), (u,v) ∈ D.graph ↔
        ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
          u =ᵐ[μ] f ∧ v =ᵐ[μ] gradient f := by
  have weighted_directional (W f g : E → ℝ) (hW : ContDiff ℝ 1 W)
      (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g)
      (hgc : HasCompactSupport g) (v : E) :
      (∫ x, Real.exp (-W x) * g x * fderiv ℝ f x v) =
        - ∫ x, Real.exp (-W x) *
          (fderiv ℝ g x v - g x * fderiv ℝ W x v) * f x := by
    let F := fun x => Real.exp (-W x) * g x
    have hF : ContDiff ℝ 1 F := hW.neg.exp.mul hg
    have hFc : HasCompactSupport F := hgc.mul_left
    have hDF : Continuous (fun x => fderiv ℝ F x v) :=
      (hF.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
    have hDf : Continuous (fun x => fderiv ℝ f x v) :=
      (hf.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
    have hDFc : HasCompactSupport (fun x => fderiv ℝ F x v) := by
      refine HasCompactSupport.of_support_subset_isCompact hFc.isCompact ?_
      intro x hx
      by_contra hn
      exact hx (by simp [fderiv_of_notMem_tsupport ℝ hn])
    have h1 : Integrable (fun x => fderiv ℝ F x v * f x) :=
      (hDF.mul hf.continuous).integrable_of_hasCompactSupport hDFc.mul_right
    have h2 : Integrable (fun x => F x * fderiv ℝ f x v) :=
      (hF.continuous.mul hDf).integrable_of_hasCompactSupport hFc.mul_right
    have h3 : Integrable (fun x => F x * f x) :=
      (hF.continuous.mul hf.continuous).integrable_of_hasCompactSupport hFc.mul_right
    have hi := integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable h1 h2 h3
      (fun x _ => hF.differentiable one_ne_zero x)
      (fun x _ => hf.differentiable one_ne_zero x)
    change (∫ x, F x * fderiv ℝ f x v) = _
    rw [hi]
    congr 1
    apply integral_congr_ae
    filter_upwards [] with x
    have hd := ((hW.differentiable one_ne_zero x).hasFDerivAt.neg.exp).mul
      (hg.differentiable one_ne_zero x).hasFDerivAt
    have he : fderiv ℝ F x v = Real.exp (-W x) *
        (fderiv ℝ g x v - g x * fderiv ℝ W x v) := by
-- Source excerpt truncated; follow the exact source link.

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

Excerpt truncated; the exact source link is authoritative.