AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ObservationConditionalKernel

No declaration docstring.

private theorem joint (M : Kernel S E) [IsMarkovKernel M]
    (sigma : S → ℝ) (hsigma : Measurable sigma)
    (update : S × (E × E) → S) (hu : Measurable update) :
    ∃ J : Kernel S (E × S), ∃ hJ : IsMarkovKernel J,
      letI := hJ
      (∀ s, J s = ((M s).prod (stdGaussian E)).map
        (fun z => (z.1+sigma s • z.2,update (s,z)))) ∧
      (∀ s, J.fst s =
        AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
          (M s) (sigma s)) ∧
      J.fst ⊗ₖ J.condKernel = J := by
  let Q : Kernel S (E × E) := M ×ₖ Kernel.const _ (stdGaussian E)
  let f : S × (E × E) → E × S :=
    fun p => (p.2.1+sigma p.1 • p.2.2,update p)
  have hf : Measurable f := ((by fun_prop : Measurable
    (fun p : S × (E × E) => p.2.1+sigma p.1 • p.2.2))).prodMk hu
  let J := (Kernel.id ×ₖ Q).map f
  have : IsMarkovKernel J := Kernel.IsMarkovKernel.map _ hf
  have hJs (s : S) : J s = ((M s).prod (stdGaussian E)).map
      (fun z => (z.1+sigma s • z.2,update (s,z))) := by
    dsimp only [J]
    rw [Kernel.map_apply _ hf,Kernel.prod_apply,Kernel.id_apply,Measure.dirac_prod,
      Measure.map_map hf (by fun_prop)]
    simp only [Q,Kernel.prod_apply,Kernel.const_apply]
    rfl
  refine ⟨J,inferInstance,hJs,?_,Kernel.disintegrate J J.condKernel⟩
  intro s
  have hfs : Measurable (fun z : E × E => (z.1+sigma s • z.2,update (s,z))) :=
    hf.comp (measurable_const.prodMk measurable_id)
  rw [Kernel.fst_apply,hJs,Measure.map_map measurable_fst hfs]
  unfold AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
    AutoSamplingTheory.TechnicalLemmas.Measure.CommonNoiseContraction.addNoise
    AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.scaledStdGaussian
  have hp := Measure.map_prod_map (M s) (stdGaussian E) measurable_id
    (by fun_prop : Measurable (fun z : E => sigma s • z))
  rw [Measure.map_id] at hp
  rw [hp,Measure.map_map (by fun_prop) (by fun_prop)]
  rfl

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ObservationConditionalKernel.lean:47published source at 0e31a3cda412

No declaration docstring.

private def firstIndex (q : ℕ → S → ℝ) (b : S → ℝ) (s : S) : ℕ := by
  classical
  exact if h : ∃ n, q n s ≤ b s then Nat.find h else 0


local notation "RefState" E:arg => ℝ≥0 × E × E × ℕ × (ℕ → E)

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ObservationConditionalKernel.lean:87published source at 0e31a3cda412

No declaration docstring.

private theorem actual_joint {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 := by
  classical
  intro d v bp obs center F T q N out update
  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
  exact joint M (fun s => Real.sqrt (τ s/((β:ℝ)+s.1))) (by fun_prop) update hu

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ObservationConditionalKernel.lean:94published source at 0e31a3cda412

No declaration docstring.

private theorem actual_conditional {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) := by
  classical
  intro d v bp obs center F T q N out update
  obtain ⟨J,hJ,hJs,hJfst,hdis⟩ := actual_joint 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
  have hobs : Measurable obs := by dsimp [obs]; fun_prop
  have hf (s : RefState E) : Measurable (fun z => (obs (s,z),update (s,z))) :=
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ObservationConditionalKernel.lean:131published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

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
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ObservationConditionalKernel.lean:195published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.