theorem
proved
tactic proof
h_theorem_recognition
show as:
view Lean formalization →
formal statement (Lean)
398theorem h_theorem_recognition
399 (sys : RecognitionSystem) (X : Ω → ℝ)
400 (p : ℝ → ProbabilityDistribution Ω)
401 (t₁ t₂ : ℝ) (h : t₁ ≤ t₂)
402 -- Assume p(t) is a valid relaxation trajectory
403 (h_relax : ∀ t ε, ε > 0 →
404 kl_divergence (p (t + ε)).p (gibbs_measure sys X) ≤
405 kl_divergence (p t).p (gibbs_measure sys X)) :
406 recognition_free_energy sys (p t₂).p X ≤ recognition_free_energy sys (p t₁).p X := by
proof body
Tactic-mode proof.
407 -- F_R(p) = F_R(Gibbs) + TR * D_KL(p || Gibbs)
408 have h_kl_identity₁ := free_energy_kl_identity sys X (p t₁)
409 have h_kl_identity₂ := free_energy_kl_identity sys X (p t₂)
410
411 by_cases heq : t₁ = t₂
412 · rw [heq]
413 · have hlt : t₁ < t₂ := lt_of_le_of_ne h heq
414 have h_kl_dec : kl_divergence (p t₂).p (gibbs_measure sys X) ≤
415 kl_divergence (p t₁).p (gibbs_measure sys X) := by
416 have := h_relax t₁ (t₂ - t₁) (sub_pos.mpr hlt)
417 simp only [add_sub_cancel] at this
418 exact this
419
420 -- F_R(p t₂) ≤ F_R(p t₁) iff F_R(p t₂) - F_R(p t₁) ≤ 0
421 rw [← sub_nonpos]
422 have : recognition_free_energy sys (p t₂).p X - recognition_free_energy sys (p t₁).p X =
423 sys.TR * (kl_divergence (p t₂).p (gibbs_measure sys X) - kl_divergence (p t₁).p (gibbs_measure sys X)) := by
424 linarith [h_kl_identity₁, h_kl_identity₂]
425 rw [this]
426 apply mul_nonpos_of_nonneg_of_nonpos
427 · exact sys.TR_pos.le
428 · linarith [h_kl_dec]
429
430/-- Status report for Free Energy Monotonicity module. -/