AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent

- 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

AutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalResolvent.lean:21published source at 0e31a3cda412