AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRepresentative

- The actual reflected pair has conditional kernel S, and the actual compressed reflection PUP of each smooth compactly supported macroscopic test has the S-expectation as an L2 representative with the score covariance derivative. All conditional and representative identities use one compatible kernel; no equality between independently existential witnesses is assumed.

theorem macroscopic_reflection_smooth_representative {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : NNReal} {η : ℝ}
    (hα : 0 < (α : ℝ)) (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 < η) :
    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 Λ := J.map (fun p : E × E => (p.2,(2:ℝ) • p.1-p.2))
    let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
      (lpMeas ℝ ℝ (MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)) 2 J).subtypeL
        ∘L condExpL2 ℝ ℝ measurable_snd.comap_le
    let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
      (1/(4*η)) • innerSL ℝ (y-u)
    ∃ S : Kernel E E, IsMarkovKernel S ∧ Λ.IsCondKernel S ∧ Λ.fst = J.snd ∧
      ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
        (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J]
          (fun p => g (p.1,(2:ℝ) • p.1-p.2))) ∧
        Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
        ∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
          ∃ g : Lp ℝ 2 J,
            (g : E × E → ℝ) =ᵐ[J] (fun p => f p.2) ∧ P g = g ∧
            ((P * U.toContinuousLinearMap * P) g : E × E → ℝ) =ᵐ[J]
              (fun p => ∫ u, f u ∂S p.2) ∧
            MemLp (fun y => ∫ u, f u ∂S y) 2 J.snd ∧
            ∀ y, Integrable (s y) (S y) ∧ Integrable (fun u => f u • s y u) (S y) ∧
              HasFDerivAt (fun z => ∫ u, f u ∂S z)
              ((∫ u, f u • s y u ∂S y) -
                (∫ u, f u ∂S y) • (∫ u, s y u ∂S y)) y := by
  have reflected_disintegration {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
      [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
      (ρ : Measure (E × E)) [IsFiniteMeasure ρ]
      (R S : Kernel E E) [IsMarkovKernel R] [IsMarkovKernel S]
      [ρ.IsCondKernel R]
      (hS : ∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) :
      let G := fun p : E × E => (p.1,(2:ℝ) • p.2-p.1)
      (ρ.map G).fst = ρ.fst ∧ (ρ.map G).IsCondKernel S := by
    let G := fun p : E × E => (p.1,(2:ℝ) • p.2-p.1)
    have hG : Measurable G := by fun_prop
    have hfst : (ρ.map G).fst = ρ.fst := by
      exact Measure.fst_map_prodMk (by fun_prop)
    have hmap : ρ.fst ⊗ₘ S = (ρ.fst ⊗ₘ R).map G := by
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/ProximalBPS/MacroscopicRepresentative.lean:27published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.