`Learning.stepsUntil_eq_leastGE`🔗

Lemma

No docstring.

theorem

Learning.stepsUntil_eq_leastGE.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {m : ℕ} (a : 𝓐) (hm : m ≠ 0) :
  stepsUntil A a m =
    MeasureTheory.leastGE (fun n ω => pullCount A a (n + 1) ω) m
Learning.stepsUntil_eq_leastGE.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {m : ℕ}
  (a : 𝓐) (hm : m ≠ 0) :
  stepsUntil A a m =
    MeasureTheory.leastGE
      (fun n ω => pullCount A a (n + 1) ω)
      m

Code

lemma stepsUntil_eq_leastGE (a : 𝓐) (hm : m ≠ 0) :
    stepsUntil A a m = leastGE (fun n (ω : Ω) ↦ pullCount A a (n + 1) ω) m

Proof

by
  classical
  ext ω
  rw [stepsUntil_eq_dite]
  unfold leastGE hittingAfter
  simp only [Nat.bot_eq_zero, zero_le, Set.mem_Ici, true_and]
  have h_iff : (∃ s, pullCount A a (s + 1) ω = m) ↔ (∃ s, m ≤ pullCount A a (s + 1) ω) := by
    refine ⟨fun ⟨s, hs⟩ ↦ ⟨s, hs.ge⟩, fun ⟨s, hs⟩ ↦ ?_⟩
    exact exists_pullCount_eq_of_le hs hm
  by_cases h_exists : ∃ s, m ≤ pullCount A a (s + 1) ω
  swap; · simp_rw [h_iff]; simp [h_exists]
  rw [ite_eq_left h_exists, dite_eq_left]
  swap; · rwa [h_iff]
  simp only [ENat.some_eq_natCast, Nat.cast_inj]
  rw [Nat.find_eq_iff]
  constructor
  · apply le_antisymm
    · by_contra! h_contra
      obtain ⟨s, hs⟩ : ∃ s, pullCount A a (s + 1) ω = m := exists_pullCount_eq_of_le h_contra.le hm
      rw [← hs] at h_contra
      refine h_contra.not_ge ?_
      gcongr
      exact csInf_le (by simp) (by simp)
    · exact Nat.sInf_mem (s := {j | m ≤ pullCount A a (j + 1) ω}) h_exists
  · intro n hn h_contra
    refine hn.not_ge ?_
    exact csInf_le (by simp) (by simp [h_contra])

Actions: Source · Open Issue

Meaning last changed in v4.34.0-rc1-3-g2cf8f3b (2026-08-20).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 2 project declarations, 29 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

Learning.stepsUntil_eq_leastGE🔗

`Learning.stepsUntil_eq_leastGE`🔗