LeanMachineLearning

Learning.pullCount_lt_of_le_stepsUntilπŸ”—

Lemma

No docstring.

πŸ”—theorem
Learning.pullCount_lt_of_le_stepsUntil.{u_1, u_3} {𝓐 : Type u_1}
  {Ξ© : Type u_3} [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} (a : 𝓐) {n m : β„•}
  (Ο‰ : Ξ©) (h_exists : βˆƒ s, pullCount A a (s + 1) Ο‰ = m)
  (hn : ↑n < stepsUntil A a m Ο‰) : pullCount A a (n + 1) Ο‰ < m
Learning.pullCount_lt_of_le_stepsUntil.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ξ© : Type u_3}
  [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} (a : 𝓐)
  {n m : β„•} (Ο‰ : Ξ©)
  (h_exists :
    βˆƒ s, pullCount A a (s + 1) Ο‰ = m)
  (hn : ↑n < stepsUntil A a m Ο‰) :
  pullCount A a (n + 1) Ο‰ < m

Code

lemma pullCount_lt_of_le_stepsUntil (a : 𝓐) {n m : β„•} (Ο‰ : Ξ©)
    (h_exists : βˆƒ s, pullCount A a (s + 1) Ο‰ = m) (hn : n < stepsUntil A a m Ο‰) :
    pullCount A a (n + 1) Ο‰ < m
Proof
by
  classical
  have h_eq := stepsUntil_eq_dite (A := A) a m Ο‰
  simp only [h_exists, ↓reduceDIte] at h_eq
  rw [← ENat.natCast_toNat (stepsUntil_ne_top h_exists)] at hn
  refine lt_of_le_of_ne ?_ ?_
  Β· calc pullCount A a (n + 1) Ο‰
    _ ≀ pullCount A a (stepsUntil A a m Ο‰ + 1).toNat Ο‰ := by
      refine monotone_pullCount a Ο‰ ?_
      rw [ENat.toNat_add (stepsUntil_ne_top h_exists) (by simp)]
      simp only [ENat.toNat_one, add_le_add_iff_right]
      exact mod_cast hn.le
    _ = m := pullCount_stepsUntil_add_one h_exists
  Β· refine Nat.find_min h_exists (m := n) ?_
    suffices n < (stepsUntil A a m Ο‰).toNat by
      rwa [h_eq, ENat.toNat_natCast] at this
    exact mod_cast hn

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, 28 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.