AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.JointReferenceGradientDescent

No declaration docstring.

private theorem joint_iterates {g : E → E} (hg : Continuous g)
    {u : E × E → E} (hu : Continuous u) (A c : ℝ) (n : ℕ) :
    Continuous (fun p : E × E =>
      (fun x => x-c⁻¹ • (g x+A⁻¹ • (x-u p)))^[n] p.1) := by
  induction n with
  | zero => simpa only [Function.iterate_zero, id_eq] using continuous_fst
  | succ n ih =>
    simp only [Function.iterate_succ_apply']
    exact ih.sub (((hg.comp ih).add ((ih.sub hu).const_smul _)).const_smul _)

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/JointReferenceGradientDescent.lean:36published source at 0e31a3cda412

No declaration docstring.

private def jointIndex (T : E × E → E → E) (g : E × E → E → ℝ)
    (s : ℝ) (p : E × E) : ℕ := by
  classical
  exact if h : ∃ n, g p ((T p)^[n] p.1) ≤ s then Nat.find h else 0

omit [CompleteSpace E] [InnerProductSpace ℝ E] in

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/JointReferenceGradientDescent.lean:46published source at 0e31a3cda412

No declaration docstring.

private theorem joint_stop [MeasurableSpace E] [BorelSpace E]
    (T : E × E → E → E) (g : E × E → E → ℝ) (s : ℝ)
    (B : E × E → ℝ)
    (hi : ∀ n : ℕ, Measurable (fun p : E × E => (T p)^[n] p.1))
    (hp : ∀ n : ℕ, MeasurableSet {p : E × E | g p ((T p)^[n] p.1) ≤ s})
    (hw : ∀ p : E × E, ∃ n : ℕ, g p ((T p)^[n] p.1) ≤ s ∧ (n:ℝ)+1 ≤ B p) :
    let N := jointIndex T g s
    Measurable N ∧ Measurable (fun p => (T p)^[N p] p.1) ∧
      ∀ p, g p ((T p)^[N p] p.1) ≤ s ∧
        (∀ j < N p, s < g p ((T p)^[j] p.1)) ∧ (N p:ℝ)+1 ≤ B p := by
  classical
  let N := jointIndex T g s
  have ht (p : E × E) : ∃ n, g p ((T p)^[n] p.1) ≤ s :=
    let ⟨n,hn,_⟩ := hw p; ⟨n,hn⟩
  have hn (p : E × E) : N p = Nat.find (ht p) := by
    simp only [N,jointIndex,dif_pos (ht p)]
  have hNm : Measurable N := by
    have he : N = fun p => Nat.find (ht p) := funext hn
    rw [he]
    exact measurable_find ht hp
  have hOm : Measurable (fun p => (T p)^[N p] p.1) := by
    have he : (fun p => (T p)^[N p] p.1) =
        (fun p => (T p)^[Nat.find (ht p)] p.1) := by funext p; rw [hn]
    rw [he]
    exact Measurable.find hi hp ht
  refine ⟨hNm,hOm,fun p => ?_⟩
  change g p ((T p)^[N p] p.1) ≤ s ∧
    (∀ j < N p, s < g p ((T p)^[j] p.1)) ∧ (N p:ℝ)+1 ≤ B p
  refine ⟨?_,?_,?_⟩
  · rw [hn]; exact Nat.find_spec (ht p)
  · intro j hj
    rw [hn] at hj
    exact lt_of_not_ge (Nat.find_min (ht p) hj)
  · obtain ⟨n,hs,hB⟩ := hw p
    have hle : N p ≤ n := by rw [hn]; exact Nat.find_min' (ht p) hs
    have hr : (N p:ℝ) ≤ n := by exact_mod_cast hle
    linarith

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/JointReferenceGradientDescent.lean:52published source at 0e31a3cda412

No declaration docstring.

private theorem actual_joint_program [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] {U : E → ℝ} {α β : ℝ≥0}
    (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
      fderiv ℝ (fderiv ℝ U) x v v ≤ (β:ℝ)*‖v‖^2)
    (hαβ : α ≤ β) {A d τ : ℝ} (hA : 0 < A) (hd : 0 < d)
    (hdim : d = Module.finrank ℝ E) :
    let u := fun p : E × E => p.1+Real.sqrt τ • p.2
    let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
    let a := (α:ℝ)+A⁻¹
    let c := (β:ℝ)+A⁻¹
    let k := c/a
    let T := fun p x => x-c⁻¹ • gradient (F p) x
    let N := jointIndex T (fun p x => ‖gradient (F p) x‖^2) (a*d)
    Measurable N ∧ Measurable (fun p => (T p)^[N p] p.1) ∧
      ∀ p, ‖gradient (F p) ((T p)^[N p] p.1)‖^2 ≤ a*d ∧
        (∀ j < N p, a*d < ‖gradient (F p) ((T p)^[j] p.1)‖^2) ∧
        (N p:ℝ)+1 ≤ k*Real.log (1+A*‖gradient (F p) p.1‖^2/d)+2 := by
  let u := fun p : E × E => p.1+Real.sqrt τ • p.2
  let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
  let a := (α:ℝ)+A⁻¹
  let c := (β:ℝ)+A⁻¹
  let k := c/a
  let T := fun p x => x-c⁻¹ • gradient (F p) x
  have H (p : E × E) :=
    TerminalReferenceGradientDescent.terminal_reference_gradient_descent
      hU hH hαβ hA hd hdim (u p)
  have hg (p : E × E) (x : E) :
      gradient (F p) x=gradient U x+A⁻¹ • (x-u p) := (H p).2.2.2.1 x
  have hu : Continuous u := continuous_fst.add (continuous_snd.const_smul _)
  have hgU : Continuous (gradient U) :=
    TechnicalLemmas.Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
      (hU.of_le (by norm_num))
  have hTeq : T = fun p x => x-c⁻¹ • (gradient U x+A⁻¹ • (x-u p)) := by
    funext p x; exact congrArg (fun z => x-c⁻¹ • z) (hg p x)
  have hi (n : ℕ) : Continuous (fun p : E × E => (T p)^[n] p.1) := by
    rw [hTeq]
    exact joint_iterates hgU hu A c n
  have hp (n : ℕ) : MeasurableSet
      {p : E × E | ‖gradient (F p) ((T p)^[n] p.1)‖^2 ≤ a*d} := by
    simp_rw [hg]
    exact measurableSet_le
      (((hgU.comp (hi n)).add (((hi n).sub hu).const_smul _)).norm.pow 2).measurable
      measurable_const
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/JointReferenceGradientDescent.lean:90published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

private theorem expected_count {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsProbabilityMeasure μ] (g : X → ℝ) (N : X → ℕ)
    {k s M : ℝ} (hk : 0 < k) (hs : 0 < s)
    (hgm : Measurable g) (hgi : Integrable g μ) (hg : ∀ x, 0 ≤ g x)
    (hNm : Measurable N) (hM : (∫ x, g x ∂μ) ≤ M)
    (hbound : ∀ x, (N x:ℝ)+1 ≤ k*Real.log (1+g x/s)+2) :
    Integrable (fun x => (N x:ℝ)+1) μ ∧
      (∫ x, (N x:ℝ)+1 ∂μ) ≤ 2+k*Real.log (1+M/s) := by
  have hM0 : 0 ≤ M := (integral_nonneg hg).trans hM
  have hden : 0 < 1+M/s := by positivity
  have hsm : 0 < s+M := by positivity
  have hpos (x : X) : 0 < 1+g x/s := by have := hg x; positivity
  have hl0 (x : X) : 0 ≤ Real.log (1+g x/s) :=
    Real.log_nonneg (by have := div_nonneg (hg x) hs.le; linarith)
  have hlub (x : X) : Real.log (1+g x/s) ≤ g x/s := by
    have := Real.log_le_sub_one_of_pos (hpos x)
    linarith
  have hlm : Measurable (fun x => Real.log (1+g x/s)) :=
    (measurable_const.add (hgm.div_const s)).log
  have hli : Integrable (fun x => Real.log (1+g x/s)) μ :=
    (hgi.div_const s).mono' hlm.aestronglyMeasurable (Filter.Eventually.of_forall fun x => by
      rw [Real.norm_eq_abs,abs_of_nonneg (hl0 x)]
      exact hlub x)
  have htangent (x : X) : Real.log (1+g x/s) ≤
      Real.log (1+M/s)+(g x-M)/(s+M) := by
    have ht := Real.log_le_sub_one_of_pos (div_pos (hpos x) hden)
    rw [Real.log_div (hpos x).ne' hden.ne'] at ht
    have he : (1+g x/s)/(1+M/s)-1=(g x-M)/(s+M) := by
      field_simp; ring
    rw [he] at ht
    linarith
  have hsubi : Integrable (fun x => g x-M) μ := hgi.sub (integrable_const M)
  have hdivi : Integrable (fun x => (g x-M)/(s+M)) μ := hsubi.div_const _
  have hri : Integrable (fun x => Real.log (1+M/s)+(g x-M)/(s+M)) μ :=
    (integrable_const _).add hdivi
  have hj := integral_mono hli hri htangent
  rw [integral_add (integrable_const _) hdivi,
    integral_div,integral_sub hgi (integrable_const M)] at hj
  simp only [integral_const,probReal_univ,smul_eq_mul,one_mul] at hj
  have hlog : (∫ x, Real.log (1+g x/s) ∂μ) ≤ Real.log (1+M/s) := by
    have hn : ((∫ x,g x ∂μ)-M)/(s+M) ≤ 0 :=
      div_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr hM) hsm.le
    linarith
  have hbi : Integrable (fun x => k*Real.log (1+g x/s)+2) μ :=
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/JointReferenceGradientDescent.lean:148published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

theorem joint_reference_gradient_descent [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] {U : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (hαβ : α ≤ β) (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
      fderiv ℝ (fderiv ℝ U) x v v ≤ (β:ℝ)*‖v‖^2)
    {η τ r : ℝ} (hη : 0 ≤ η) (hτ : 0 < τ) (hr : 0 ≤ r)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (ν : Measure E) [IsProbabilityMeasure ν]
    (hw : TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance ν
      (TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        ((volume : Measure E).tilted (fun x => -U x)) (Real.sqrt η)) ^ 2 ≤ ENNReal.ofReal (r^2)) :
    let d : ℝ := Module.finrank ℝ E
    let A := η+τ
    let a := (α:ℝ)+A⁻¹
    let c := (β:ℝ)+A⁻¹
    let k := c/a
    let M := 4*(β:ℝ)*d+4*(β:ℝ)^2*η*d+2*(β:ℝ)^2*r^2
    let u := fun p : E × E => p.1+Real.sqrt τ • p.2
    let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
    let T := fun p x => x-c⁻¹ • gradient (F p) x
    let N := jointIndex T (fun p x => ‖gradient (F p) x‖^2) (a*d)
    let out := fun p => (T p)^[N p] p.1
    Measurable N ∧ Measurable out ∧
      (∀ p, ‖gradient (F p) (out p)‖^2 ≤ a*d ∧
        ‖u p-A • gradient U (out p)-out p‖ = A*‖gradient (F p) (out p)‖ ∧
        ‖u p-A • gradient U (out p)-out p‖ ≤ A*Real.sqrt (a*d) ∧
        (∀ j < N p, a*d < ‖gradient (F p) ((T p)^[j] p.1)‖^2) ∧
        (N p:ℝ)+1 ≤ k*Real.log (1+A*‖gradient (F p) p.1‖^2/d)+2) ∧
      Integrable (fun p => (N p:ℝ)+1) (ν.prod (stdGaussian E)) ∧
      (∫ p, (N p:ℝ)+1 ∂ν.prod (stdGaussian E)) ≤
        2+k*Real.log (1+A*(M+τ*d/A^2)/d) := by
  let d : ℝ := Module.finrank ℝ E
  let A := η+τ
  let a := (α:ℝ)+A⁻¹
  let c := (β:ℝ)+A⁻¹
  let k := c/a
  let M := 4*(β:ℝ)*d+4*(β:ℝ)^2*η*d+2*(β:ℝ)^2*r^2
  let u := fun p : E × E => p.1+Real.sqrt τ • p.2
  let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
  let T := fun p x => x-c⁻¹ • gradient (F p) x
  let N := jointIndex T (fun p x => ‖gradient (F p) x‖^2) (a*d)
  let out := fun p => (T p)^[N p] p.1
  have hA : 0 < A := add_pos_of_nonneg_of_pos hη hτ
  have ha : 0 < a := add_pos_of_nonneg_of_pos α.coe_nonneg (inv_pos.mpr hA)
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/JointReferenceGradientDescent.lean:207published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.