AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveKLError

- Construct the ideal center-dependent kernels and bound the actual composed output KL by the input KL plus the conditional KL integrated under that actual input law. No finite-divergence or separately assumed measurability premise.

theorem adaptive_center_kl_error {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ) (hb : 0 ≤ b) (ha : 0 < a) :
    ∃ (T H : Kernel E E) (B : Kernel (E × E) (E × E)),
      IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
      (∀ u, T u = μ.tilted (fun x => -(b/2)*‖x-u‖^2)) ∧
      (∀ u, H u = GaussianSmoothing.gaussianSmoothing (T u) (Real.sqrt a)) ∧
      (∀ u y, B (u,y) = Measure.map (Prod.mk u)
        ((T u).tilted (fun x => -‖x-y‖^2/(2*a)))) ∧
      (∀ u y, B (u,y) = Measure.map (Prod.mk u)
        (μ.tilted (fun x => -((b+a⁻¹)/2)*
          ‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2))) ∧
      (∀ (ν : Measure E), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T) ∧
      ∀ (ν : Measure E), IsProbabilityMeasure ν →
        ∀ (P : Measure (E × E)), IsProbabilityMeasure P →
        ∀ (L : Kernel (E × E) (E × E)), IsMarkovKernel L →
          Measurable (fun s => klDiv (L s) (B s)) ∧
          klDiv (L ∘ₘ P) (ν ⊗ₘ T) ≤ klDiv P (ν ⊗ₘ H) + ∫⁻ s, klDiv (L s) (B s) ∂P := by
  have measurable_fiber_kl (L K : Kernel (E × E) (E × E)) [IsMarkovKernel L] [IsMarkovKernel K] :
      Measurable (fun x => klDiv (L x) (K x)) := by
    classical
    have hf : Measurable (fun p : (E × E) × (E × E) =>
        ENNReal.ofReal (klFun ((Kernel.rnDeriv L K p.1 p.2).toReal))) := by
      exact ENNReal.measurable_ofReal.comp
        (continuous_klFun.measurable.comp (Kernel.measurable_rnDeriv L K).ennreal_toReal)
    have heq (x : (E × E)) : klDiv (L x) (K x) =
        if L x ≪ K x then ∫⁻ y, ENNReal.ofReal (klFun ((Kernel.rnDeriv L K x y).toReal)) ∂K x
        else ∞ := by
      rw [klDiv_eq_lintegral_klFun]
      split_ifs
      · apply lintegral_congr_ae
        filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := L) (η := K) (a := x)] with y hy
        rw [hy]
      · rfl
    simp_rw [heq]
    exact Measurable.ite (Kernel.measurableSet_absolutelyContinuous L K)
      hf.lintegral_kernel_prod_right' measurable_const


  have conditional_kl_integral (μ : Measure (E × E)) [IsProbabilityMeasure μ]
      (L K : Kernel (E × E) (E × E)) [IsMarkovKernel L] [IsMarkovKernel K] :
      klDiv (μ ⊗ₘ L) (μ ⊗ₘ K) = ∫⁻ x, klDiv (L x) (K x) ∂μ := by
    classical
    by_cases hac : μ ⊗ₘ L ≪ μ ⊗ₘ K
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/AdaptiveKLError.lean:28published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.