AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeak

No declaration docstring.

private theorem compact_directional_ibp (W f φ : E → ℝ)
    (hW : ContDiff ℝ 1 W) (hf : ContDiff ℝ 1 f) (hφ : ContDiff ℝ 1 φ)
    (hc : HasCompactSupport φ) (v : E) :
    (∫ x, Real.exp (-W x) * φ x * fderiv ℝ f x v) =
      - ∫ x, Real.exp (-W x) *
        (fderiv ℝ φ x v - φ x * fderiv ℝ W x v) * f x := by
  let F := fun x => Real.exp (-W x) * φ x
  have hF : ContDiff ℝ 1 F := hW.neg.exp.mul hφ
  have hFc : HasCompactSupport F := hc.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
    (hφ.differentiable one_ne_zero x).hasFDerivAt
  have he : fderiv ℝ F x v = Real.exp (-W x) *
      (fderiv ℝ φ x v - φ x * fderiv ℝ W x v) := by
    rw [show fderiv ℝ F x = _ from hd.fderiv]
    simp only [add_apply, smul_apply, neg_apply, smul_eq_mul, Pi.neg_apply]
    ring
  rw [he]

/-- Every member of the same closed gradient graph satisfies weighted compact
test integration by parts, with both integrands genuinely integrable. The exact
original graph is the already constructed smooth core, not an assumed IBP law. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedGradientWeak.lean:22published source at 0e31a3cda412

- Every member of the same closed gradient graph satisfies weighted compact test integration by parts, with both integrands genuinely integrable. The exact original graph is the already constructed smooth core, not an assumed IBP law.

theorem closed_gradient_weighted_ibp (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 μ), D.IsClosable →
      (∀ (u : Lp ℝ 2 μ) (G : Lp E 2 μ), (u,G) ∈ D.graph ↔
        ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
          u =ᵐ[μ] f ∧ G =ᵐ[μ] gradient f) →
      ∀ (u : Lp ℝ 2 μ) (G : Lp E 2 μ), (u,G) ∈ D.closure.graph →
      ∀ (φ : E → ℝ), ContDiff ℝ 1 φ → HasCompactSupport φ → ∀ v : E,
        Integrable (fun x => φ x * inner ℝ (G x) v) μ ∧
        Integrable (fun x => u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v)) μ ∧
        (∫ x, φ x * inner ℝ (G x) v ∂μ) =
          - ∫ x, u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v) ∂μ := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  dsimp only
  intro D hD hgraph u G hu φ hφ hc v
  let P := fun x => φ x • v
  let q := fun x => fderiv ℝ φ x v - φ x * fderiv ℝ W x v
  have hP : Continuous P := hφ.continuous.smul continuous_const
  have hPc : HasCompactSupport P := hc.smul_right
  have hdφ : Continuous (fun x => fderiv ℝ φ x v) :=
    (hφ.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
  have hdW : Continuous (fun x => fderiv ℝ W x v) :=
    (hW.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
  have hdc : HasCompactSupport (fun x => fderiv ℝ φ x v) := by
    refine HasCompactSupport.of_support_subset_isCompact hc.isCompact ?_
    intro x hx
    by_contra hn
    exact hx (by simp [fderiv_of_notMem_tsupport ℝ hn])
  have hq : Continuous q := hdφ.sub (hφ.continuous.mul hdW)
  have hqc : HasCompactSupport q := hdc.sub hc.mul_right
  have hPL : MemLp P 2 μ := hP.memLp_of_hasCompactSupport hPc
  have hqL : MemLp q 2 μ := hq.memLp_of_hasCompactSupport hqc
  let pv : Lp E 2 μ := hPL.toLp P
  let qv : Lp ℝ 2 μ := hqL.toLp q
  have hPe (H : Lp E 2 μ) :
      (fun x => inner ℝ (H x) (pv x)) =ᵐ[μ] (fun x => φ x * inner ℝ (H x) v) := by
    filter_upwards [hPL.coeFn_toLp] with x hx
    rw [show pv x = P x from hx]
    simp [P, inner_smul_right]
  have hqe (a : Lp ℝ 2 μ) :
      (fun x => inner ℝ (a x) (qv x)) =ᵐ[μ] (fun x => a x * q x) := by
    filter_upwards [hqL.coeFn_toLp] with x hx
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedGradientWeak.lean:66published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.