AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL

No declaration docstring.

private theorem klFun_le_square {x : ℝ} (hx : 0 ≤ x) : klFun x ≤ (x-1)^2 := by
  rcases eq_or_lt_of_le hx with h | h
  · subst x
    norm_num [klFun_zero]
  · have he := mul_le_mul_of_nonneg_left (Real.log_le_sub_one_of_pos h) hx
    rw [klFun_apply]
    nlinarith

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:48published source at 0e31a3cda412

No declaration docstring.

private theorem kl_le_second_moment {X : Type*} [MeasurableSpace X]
    (μ ν : Measure X) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (hac : μ ≪ ν) (eps : ℝ)
    (hI : Integrable (fun x => ((μ.rnDeriv ν x).toReal)^2) ν)
    (hB : (∫ x, ((μ.rnDeriv ν x).toReal)^2 ∂ν) ≤ 1+eps^2) :
    klDiv μ ν ≤ ENNReal.ofReal (eps^2) := by
  let r := fun x => (μ.rnDeriv ν x).toReal
  have hr : Integrable r ν := by
    simpa [r] using Measure.integrableOn_toReal_rnDeriv
      (μ := μ) (ν := ν) (s := Set.univ) (measure_ne_top μ Set.univ)
  have hmass : (∫ x, r x ∂ν) = 1 := by
    simpa [r] using Measure.integral_toReal_rnDeriv hac
  have h2 : Integrable (fun x => r x^2) ν := hI
  have hlin : Integrable (fun x => 2*r x) ν := hr.const_mul 2
  have hpoly : Integrable (fun x => r x^2-2*r x) ν := h2.sub hlin
  have heq : (fun x => (r x-1)^2) = (fun x => r x^2-2*r x+1) := by
    funext x
    ring
  have hsq : Integrable (fun x => (r x-1)^2) ν := by
    rw [heq]
    exact hpoly.add (integrable_const 1)
  have hint : (∫ x, (r x-1)^2 ∂ν) ≤ eps^2 := by
    rw [heq, integral_add hpoly (integrable_const 1),
      integral_sub h2 hlin, integral_const_mul, hmass]
    simp only [integral_const, probReal_univ, smul_eq_mul, one_mul]
    change (∫ x, r x^2 ∂ν) ≤ 1+eps^2 at hB
    linarith
  rw [klDiv_eq_lintegral_klFun_of_ac hac]
  calc
    _ ≤ ∫⁻ x, ENNReal.ofReal ((r x-1)^2) ∂ν := by
      apply lintegral_mono
      intro x
      exact ENNReal.ofReal_le_ofReal (klFun_le_square ENNReal.toReal_nonneg)
    _ = ENNReal.ofReal (∫ x, (r x-1)^2 ∂ν) :=
      (ofReal_integral_eq_lintegral_ofReal hsq (ae_of_all _ fun x => sq_nonneg _)).symm
    _ ≤ ENNReal.ofReal (eps^2) := ENNReal.ofReal_le_ofReal hint

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
open MeasureTheory ProbabilityTheory InformationTheory
open scoped ENNReal NNReal
noncomputable section
namespace AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:56published source at 0e31a3cda412

No declaration docstring.

private theorem actual_terminal_target (V : E → ℝ) (hV : Differentiable ℝ V)
    (β : ℝ≥0) (hlip : LipschitzWith β (gradient V))
    [IsProbabilityMeasure ((volume : Measure E).tilted (fun x => -V x))]
    (b : ℝ) (hb : 0 < b) (hstep : (β:ℝ)*b⁻¹ < 1) (u : E) :
    (((volume : Measure E).tilted (fun x => -V x)).tilted
      (fun x => -b/2*‖x-u‖^2)) =
    ((stdGaussian E).map (fun z => u+Real.sqrt b⁻¹ • z)).tilted (fun x => -V x) := by
  have hI : Integrable (fun x => Real.exp (-V x)) (volume : Measure E) := by
    by_contra h
    have hz := tilted_of_not_integrable h
    have hm := measure_univ (μ := (volume : Measure E).tilted (fun x => -V x))
    rw [hz] at hm
    simp at hm
  have hi := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.IdealRGOIdentification.ideal_rgo_identification
    V hV β hlip b⁻¹ (inv_pos.2 hb) hstep u u
  obtain ⟨_,_,_,_,_,_,heq,hvol⟩ := hi
  rw [tilted_tilted hI]
  have hf : ((fun x => -V x)+(fun x => -b/2*‖x-u‖^2)) =
      (fun x => -(V x+‖x-u‖^2/(2*b⁻¹))) := by
    funext x
    simp only [Pi.add_apply]
    field_simp
    ring
  rw [hf, Measure.tilted]
  exact hvol.symm.trans heq

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
open MeasureTheory ProbabilityTheory InformationTheory
open scoped ENNReal NNReal
noncomputable section
universe u
namespace AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:101published source at 0e31a3cda412

No declaration docstring.

private theorem kernel_error_sum {A : Type u} [MeasurableSpace A] (P : Kernel A A) [IsMarkovKernel P]
    (e t : A → ℝ≥0∞) (he : Measurable e) (ht : Measurable t)
    (f : ℕ → A → ℝ≥0∞) (hzero : ∀ s, f 0 s ≤ t s)
    (hstep : ∀ n s, f (n+1) s ≤ e s + ∫⁻ x, f n x ∂P s) :
    ∀ n s, f n s ≤ (∑ j ∈ Finset.range n, ∫⁻ x, e x ∂(P^j) s) + ∫⁻ x, t x ∂(P^n) s := by
  have hp (n : ℕ) : IsMarkovKernel (P^n) := by
    induction n with
    | zero => change IsMarkovKernel Kernel.id; infer_instance
    | succ n ih =>
      let := ih
      rw [pow_succ]
      change IsMarkovKernel ((P^n) ∘ₖ P)
      infer_instance
  let := hp
  have hi (n : ℕ) : Measurable (fun s => ∫⁻ x, e x ∂(P^n) s) := he.lintegral_kernel
  intro n
  induction n with
  | zero =>
    intro s
    simp only [Finset.range_zero,Finset.sum_empty,zero_add,pow_zero]
    change f 0 s ≤ ∫⁻ x, t x ∂Measure.dirac s
    simpa only [lintegral_dirac' s ht] using hzero s
  | succ n ih =>
    intro s
    calc
      f (n+1) s ≤ e s + ∫⁻ x, f n x ∂P s := hstep n s
      _ ≤ e s + ∫⁻ x, (∑ j ∈ Finset.range n, ∫⁻ y, e y ∂(P^j) x) +
          ∫⁻ y, t y ∂(P^n) x ∂P s := add_le_add le_rfl (lintegral_mono ih)
      _ = _ := by
        rw [lintegral_add_left (Finset.measurable_sum _ (fun j _ => hi j))]
        rw [lintegral_finsetSum _ (fun j _ => hi j)]
        have hei (j : ℕ) : (∫⁻ x, ∫⁻ y, e y ∂(P^j) x ∂P s) = ∫⁻ y, e y ∂(P^(j+1)) s := by
          rw [pow_succ]
          exact (Kernel.lintegral_comp (P^j) P s he).symm
        have hti : (∫⁻ x, ∫⁻ y, t y ∂(P^n) x ∂P s) = ∫⁻ y, t y ∂(P^(n+1)) s := by
          rw [pow_succ]
          exact (Kernel.lintegral_comp (P^n) P s ht).symm
        simp_rw [hei]
        rw [hti,Finset.sum_range_succ']
        simp only [pow_zero]
        rw [show (1 : Kernel A A) s = Measure.dirac s from rfl,lintegral_dirac' s he]
        change e s + ((∑ j ∈ Finset.range n, ∫⁻ x, e x ∂(P^(j+1)) s) + _) =
          ((∑ j ∈ Finset.range n, ∫⁻ x, e x ∂(P^(j+1)) s) + e s) + _
        ac_rfl

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:133published source at 0e31a3cda412

No declaration docstring.

private theorem composed_error_sum {S E : Type u} [MeasurableSpace S] [MeasurableSpace E]
    (P : Kernel S S) (T L : Kernel S E)
    [IsMarkovKernel P] [IsMarkovKernel T] [IsMarkovKernel L]
    (e : S → ℝ≥0∞) (he : Measurable e)
    (hstep : ∀ R : Kernel S E, IsMarkovKernel R →
      Measurable (fun s => klDiv (R s) (T s)) ∧
      ∀ s, klDiv ((R ∘ₖ P) s) (T s) ≤ e s+∫⁻ t, klDiv (R t) (T t) ∂P s) :
    ∀ n s, klDiv ((L ∘ₖ (P^n)) s) (T s) ≤
      (∑ j ∈ Finset.range n, ∫⁻ t, e t ∂(P^j) s)+
      ∫⁻ t, klDiv (L t) (T t) ∂(P^n) s := by
  have hp (n : ℕ) : IsMarkovKernel (P^n) := by
    induction n with
    | zero => change IsMarkovKernel Kernel.id; infer_instance
    | succ n ih =>
      let := ih
      rw [pow_succ]
      change IsMarkovKernel ((P^n) ∘ₖ P)
      infer_instance
  let := hp
  apply kernel_error_sum P e (fun s => klDiv (L s) (T s)) he (hstep L inferInstance).1
    (fun n s => klDiv ((L ∘ₖ (P^n)) s) (T s))
  · intro s
    rw [pow_zero]
    change klDiv ((L ∘ₖ Kernel.id) s) (T s) ≤ klDiv (L s) (T s)
    rw [Kernel.comp_id]
  · intro n s
    have h := (hstep (L ∘ₖ (P^n)) inferInstance).2 s
    rw [pow_succ]
    change klDiv ((L ∘ₖ ((P^n) ∘ₖ P)) s) (T s) ≤ _
    rw [← Kernel.comp_assoc]
    exact h

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
open MeasureTheory ProbabilityTheory InformationTheory
open scoped ENNReal NNReal
noncomputable section
namespace AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:177published source at 0e31a3cda412

No declaration docstring.

private theorem terminal_precision_large (κ b0 : ℝ≥0) (hκ : 1 ≤ κ)
    (d Δ : ℝ) (hd : 1 ≤ d) (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) :
    let K := (1+(b0:ℝ))/((κ:ℝ)⁻¹+b0)
    let L := 2+Real.log (K*d*2/Δ)
    let B := (1/1024)/(Real.sqrt (d*L)+L)
    0 < B ∧ 1 < B⁻¹ := by
  intro K L B
  have hk : (1:ℝ) ≤ κ := by exact_mod_cast hκ
  have hk0 : 0 < (κ:ℝ) := lt_of_lt_of_le zero_lt_one hk
  have hki : (κ:ℝ)⁻¹ ≤ 1 := (inv_le_one₀ hk0).2 hk
  have hden : 0 < (κ:ℝ)⁻¹+(b0:ℝ) := add_pos_of_pos_of_nonneg (inv_pos.2 hk0) b0.coe_nonneg
  have hK : 1 ≤ K := by
    apply (le_div_iff₀ hden).2
    linarith
  have hprod : 1 ≤ K*d := by nlinarith
  have harg : 1 ≤ K*d*2/Δ := by
    apply (le_div_iff₀ hΔ).2
    linarith
  have hL : 2 ≤ L := by
    dsimp only [L]
    linarith [Real.log_nonneg harg]
  have hs : 0 ≤ Real.sqrt (d*L) := Real.sqrt_nonneg _
  have hb0 : 0 < B := div_pos (by norm_num) (by linarith)
  refine ⟨hb0,?_⟩
  apply (one_lt_inv₀ hb0).2
  apply (div_lt_one (by linarith : 0 < Real.sqrt (d*L)+L)).2
  linarith

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
open Set
namespace AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
variable {E S X : Type*} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [BorelSpace E] [MeasurableSpace S] [MeasurableSpace X]

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:214published source at 0e31a3cda412

No declaration docstring.

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

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:247published source at 0e31a3cda412

No declaration docstring.

private def scaledCached (V : E → ℝ) (A : S → ℝ) (h g : S → E)
    (p : (S × E) × (ℝ × E)) : ℝ :=
  let s := p.1.1
  let x := p.1.2
  let t := p.2.1
  let z := Real.sqrt (A s) • p.2.2
  inner ℝ ((Real.pi/2) • (Real.cos (Real.pi/2*t) • (x-h s)-
    Real.sin (Real.pi/2*t) • z))
    (g s-gradient V (h s+Real.sin (Real.pi/2*t) • (x-h s)+
      Real.cos (Real.pi/2*t) • z))

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:251published source at 0e31a3cda412

No declaration docstring.

private abbrev Attempt (X A : Type*) := X × (ℕ × ((ℕ → A) × ℝ))

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:262published source at 0e31a3cda412

No declaration docstring.

private def attemptLaw {X A : Type*} [MeasurableSpace X] [MeasurableSpace A]
    (q : Measure X) (nu : Measure A) (B : ℝ) (hB : 0 < B) : Measure (Attempt X A) :=
  q.prod ((poissonMeasure (⟨2*B, by positivity⟩ : ℝ≥0)).prod
    ((Measure.infinitePi (fun _ : ℕ => nu)).prod (volume.restrict (Set.Icc 0 1))))

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:264published source at 0e31a3cda412

No declaration docstring.

private def accepted {X A : Type*} (W : X × A → ℝ) (B : ℝ) : Set (Attempt X A) :=
  {p | p.2.2.2 ≤ ∏ i : Fin p.2.1, (B+W (p.1,p.2.2.1 i.val))/(2*B)}

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:269published source at 0e31a3cda412

No declaration docstring.

private def output {X A : Type*} (W : X × A → ℝ) (B : ℝ) (x0 : X)
    (omega : ℕ → Attempt X A) : X := by
  classical
  exact if h : ∃ n, omega n ∈ accepted W B then (omega (Nat.find h)).1 else x0


local notation "S" => ℝ≥0 × E × E × ℕ × (ℕ → E)
set_option maxHeartbeats 2000000 in

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:272published source at 0e31a3cda412

No declaration docstring.

theorem finite_output_kl {V : E → ℝ} (κ : ℝ≥0) (hκ : 1 ≤ κ)
    (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)
    (η : S → ℝ) (hηm : Measurable η) (c Δ : ℝ)
    (hc : 0 < c) (hc1 : c < 1/4) (hη : ∀ s, 0 < η s ∧ η s ≤ c)
    (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2)
    (s0 : S) (M : Kernel S E) [IsMarkovKernel M] :
    let d : ℝ := Module.finrank ℝ E
    let K := fun r : ℝ => (1+r)/((κ:ℝ)⁻¹+r)
    let τ := fun s : S => if 2 ≤ K s.1 then K s.1 else c
    let L := (2:ℝ)+Real.log (K s0.1*d*(2:ℝ)/Δ)
    let B := (1/1024)/(Real.sqrt (d*L)+L)
    let J := Nat.ceil (8*Real.log (Real.exp 1*K s0.1/B))
    let _eps := Δ/Real.sqrt ((J:ℝ)+1)
    let v := fun s : S => (η s+τ s)/(1+s.1)
    let bp := fun s : S => s.1+Real.toNNReal (v s)⁻¹
    let obs := fun p : S × (E × E) => p.2.1+Real.sqrt (τ p.1/(1+p.1.1)) • p.2.2
    let center := fun p : S × (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-(1+(bp p.1:ℝ))⁻¹ • gradient (F p) x
    let Qn := fun n p => ‖gradient (F p) ((T p)^[n] p.2.1)‖^2
    let N := firstIndex Qn (fun p => ((κ:ℝ)⁻¹+bp p.1)*d)
    let update := fun p : S × (E × E) =>
      (bp p.1,center p,(T p)^[N p] p.2.1,p.1.2.2.2.1+1,
        fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    let bb := fun s : S => max (s.1:ℝ) B⁻¹
    let TF := fun s x => V x+bb s/2*‖x-s.2.1‖^2
    let TT := fun s x => x-(1+bb s)⁻¹ • gradient (TF s) x
    let TQn := fun n s => ‖gradient (TF s) ((TT s)^[n] (s.2.2.1))‖^2
    let TN := firstIndex TQn (fun s => d*bb s)
    let txp := fun s => (TT s)^[TN s] (s.2.2.1)
    let TA := fun s => (bb s)⁻¹
    let tg := fun s => gradient V (txp s)
    let th := fun s => s.2.1-TA s • tg s
    let tnu := (volume.restrict (Ioc (0 : ℝ) 1)).prod (stdGaussian E)
    let tW := fun s (p : E × (ℝ × E)) => min 1 (max (-1) (scaledCached V TA th tg ((s,p.1),p.2)))
    let tproposal := fun s => (stdGaussian E).map (fun z => th s+Real.sqrt (TA s) • z)
    let trho := fun s => Measure.infinitePi (fun _ : ℕ => attemptLaw (tproposal s) tnu 1 (by norm_num))
    let _tpi := fun s => ((stdGaussian E).map (fun z => s.2.1+Real.sqrt (TA s) • z)).tilted (fun x => -V x)
    let μV := (volume : Measure E).tilted (fun x => -V x)
    IsProbabilityMeasure μV ∧
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean:280published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.