ObservationConditionalKernel: mathematical reading route

Measurable product pushforward, parameterized disintegration, AE conditional support and nonnegative integration on the actual active branch.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem observation_conditional_kernel {V : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x w : E, (α:ℝ)*‖w‖^2 ≤ fderiv ℝ (fderiv ℝ V) x w w ∧
      fderiv ℝ (fderiv ℝ V) x w w ≤ (β:ℝ)*‖w‖^2)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (η τ : RefState E → ℝ) (hη : Measurable η) (hτ : Measurable τ)
    (hη0 : ∀ s, 0 < η s) (hτ0 : ∀ s, 0 < τ s)
    (M : Kernel (RefState E) E) [IsMarkovKernel M] (threshold : ℝ≥0) :
    let d : ℝ := Module.finrank ℝ E
    let v := fun s : RefState E => (η s+τ s)/((β:ℝ)+s.1)
    let bp := fun s : RefState E => s.1+Real.toNNReal (v s)⁻¹
    let obs := fun p : RefState E × (E × E) => p.2.1+Real.sqrt (τ p.1/((β:ℝ)+p.1.1)) • p.2.2
    let center := fun p : RefState E × (E × E) => (bp p.1:ℝ)⁻¹ •
      ((p.1.1:ℝ) • p.1.2.1+(v p.1)⁻¹ • obs p)
    let F := fun p x => V x+(bp p.1:ℝ)/2*‖x-center p‖^2
    let T := fun p x => x-((β:ℝ)+bp p.1)⁻¹ • gradient (F p) x
    let q := fun n p => ‖gradient (F p) ((T p)^[n] p.2.1)‖^2
    let N := firstIndex q (fun p => ((α:ℝ)+bp p.1)*d)
    let out := fun p => (T p)^[N p] p.2.1
    let update := fun p : RefState E × (E × E) =>
      (bp p.1,center p,out p,p.1.2.2.2.1+1,fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    ∃ J : Kernel (RefState E) (E × RefState E), ∃ hJ : IsMarkovKernel J,
      letI := hJ
      (∀ s, J s = ((M s).prod (stdGaussian E)).map
        (fun z => (obs (s,z),update (s,z)))) ∧
      (∀ s, J.fst s =
        AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
          (M s) (Real.sqrt (τ s/((β:ℝ)+s.1)))) ∧
      J.fst ⊗ₖ J.condKernel = J ∧
      (∀ s, ∀ᵐ y ∂J.fst s, ∀ᵐ t ∂J.condKernel (s,y),
        t.1=bp s ∧ t.2.1=(bp s:ℝ)⁻¹ • ((s.1:ℝ) • s.2.1+(v s)⁻¹ • y)) ∧
      (∀ (R : Kernel (RefState E) E) [IsMarkovKernel R] (s : RefState E)
        (A : Set E), MeasurableSet A →
        (∫⁻ z, R (update (s,z)) A ∂(M s).prod (stdGaussian E)) =
        ∫⁻ y, ∫⁻ t, R t A ∂J.condKernel (s,y) ∂J.fst s) ∧
      ∃ P : Kernel (RefState E) (RefState E), ∃ hP : IsMarkovKernel P,
        letI := hP
        (∀ s, P s=if threshold ≤ s.1 then Measure.dirac s else
          ((M s).prod (stdGaussian E)).map (fun z => update (s,z))) ∧
        ∀ (R : Kernel (RefState E) E) [IsMarkovKernel R] (s : RefState E),
          s.1 < threshold → ∀ A : Set E, MeasurableSet A →
          (R ∘ₖ P) s A = ∫⁻ y, ∫⁻ t, R t A ∂J.condKernel (s,y) ∂J.fst s := by
  classical
  intro d v bp obs center F T q N out update
  obtain ⟨J,hJ,hJs,hJfst,hdis,hsupp,hfactor⟩ :=
    actual_conditional hα hαβ hV hH hd η τ hη hτ hη0 hτ0 M threshold
  let := hJ
  have href := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernel.reference_carrying_kernel
    hα hαβ hV hH hd η τ hη hτ hη0 hτ0 M threshold
  have hu : Measurable update := href.2.2.2.1
  obtain ⟨P,hP,hPs,hproj⟩ := href.2.2.2.2.2
  let := hP
  refine ⟨J,hJ,hJs,hJfst,hdis,hsupp,hfactor,P,hP,hPs,?_⟩
  intro R hR s hs A hA
  rw [Kernel.comp_apply' R P s hA,hPs s,if_neg (not_le.mpr hs)]
  change (∫⁻ t, R t A ∂(((M s).prod (stdGaussian E)).map
    (fun z => update (s,z)))) = _
  have hum : Measurable (fun z : E × E => update (s,z)) :=
    hu.comp (measurable_const.prodMk measurable_id)
  rw [lintegral_map (R.measurable_coe hA) hum]
  exact hfactor R s A hA

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ObservationConditionalKernel

Exact module and namespace context