AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent

import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent

/-!
# Weak resolvent for the actual PBPS conditional closed gradient

Retain the same conditional kernels and the exact smooth compact gradient
operator from ConditionalGradient. For each fiber, its closure supplies the
weak equation for every positive epsilon and scalar L2 input, with uniqueness
and explicit ambient L2 energy/norm bounds. No measurable selection in y,
classical PDE solution, generator core, Bochner extension or Poincare theorem
is claimed. This is an analytic prerequisite to arXiv:2609.06905v1 Appendix C.1.
-/

namespace AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent
open MeasureTheory ProbabilityTheory InnerProductSpace
open scoped ContDiff NNReal RealInnerProductSpace Topology

/-- On each actual fiber, one fixed genuine gradient closure solves every
positive-epsilon weak equation; the operator precedes epsilon and input f. -/
theorem conditional_weak_resolvent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : NNReal} {η : ℝ}
    (hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β:ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β:ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
    let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
      ∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
        ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
        0 < (∫ u, Real.exp (-W y u)) ∧
        ∃ D : Lp ℝ 2 (S y) →ₗ.[ℝ] Lp E 2 (S y),
          Dense (D.domain : Set (Lp ℝ 2 (S y))) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
          (∀ (u : Lp ℝ 2 (S y)) (v : Lp E 2 (S y)), (u,v) ∈ D.graph ↔
            ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
              u =ᵐ[S y] f ∧ v =ᵐ[S y] gradient f) ∧
          ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 (S y),
            ∃ u : D.closure.domain,
              (∀ v : D.closure.domain, ε * ⟪(u : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
                ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) ∧
              ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 = ⟪f, (u : Lp ℝ 2 (S y))⟫ ∧
              ‖(u : Lp ℝ 2 (S y))‖ ≤ ε⁻¹ * ‖f‖ ∧
              ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
              ∀ w : D.closure.domain,
                (∀ v : D.closure.domain, ε * ⟪(w : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
                  ⟪D.closure w, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) → w = u := by
  obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
    ConditionalGradient.conditional_gradient_closable hα hαβ hV hH hη hβη
  dsimp only
  refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
  intro y
  obtain ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph⟩ := hfiber y
  refine ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph,?_⟩
  intro ε hε f
  exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent.weak_resolvent D.closure hClosed ε hε f

end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent