AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolvent

- The genuine positive-epsilon resolvent has an ordinary weak gradient and satisfies the weighted divergence-form equation, with all three test products integrable for volume. The same partial operator is retained throughout.

theorem weak_resolvent_distributional {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (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 →
      (∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) →
      ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 μ,
      ∃ u : D.closure.domain,
        (∀ v : D.closure.domain,
          ε * ⟪(u : Lp ℝ 2 μ), (v : Lp ℝ 2 μ)⟫ +
            ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 μ)⟫) ∧
        LocallyIntegrable (fun x => (u : Lp ℝ 2 μ) x) ∧
        LocallyIntegrable (fun x => D.closure u x) ∧
        (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (D.closure u x) v) ∧
          Integrable (fun x => (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (D.closure u x) v) =
            - ∫ x, (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
        ∀ ψ : E → ℝ, ContDiff ℝ ∞ ψ → HasCompactSupport ψ →
          Integrable (fun x => Real.exp (-W x) * ((u : Lp ℝ 2 μ) x * ψ x)) ∧
          Integrable (fun x => Real.exp (-W x) * inner ℝ (D.closure u x) (gradient ψ x)) ∧
          Integrable (fun x => Real.exp (-W x) * (f x * ψ x)) ∧
          ε * (∫ x, Real.exp (-W x) * ((u : Lp ℝ 2 μ) x * ψ x)) +
            (∫ x, Real.exp (-W x) * inner ℝ (D.closure u x) (gradient ψ x)) =
            ∫ x, Real.exp (-W x) * (f x * ψ x) := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph ε hε f
  let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  obtain ⟨u,hu,_⟩ := ClosedGraphResolvent.weak_resolvent D.closure hD.closure_isClosed ε hε f
  obtain ⟨huL,hGL,hderiv⟩ := WeightedGradientDistribution.closed_gradient_distributional
    W hW hI D hD hgraph u (D.closure u) (D.closure.mem_graph u)
  refine ⟨u,hu,huL,hGL,hderiv,?_⟩
  intro ψ hψ hc
  have hgCont : Continuous (gradient ψ) :=
    (toDual ℝ E).symm.continuous.comp
      (((contDiff_infty.mp hψ 1).fderiv_right (m := 0) (by norm_num)).continuous)
  have hgComp : HasCompactSupport (gradient ψ) := by
    refine HasCompactSupport.of_support_subset_isCompact hc.isCompact ?_
    intro x hx
-- Source excerpt truncated; follow the exact source link.

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

Excerpt truncated; the exact source link is authoritative.