Source indexedlemma · leanprover/lean4:v4.32.0

my_other_markov

APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:80 to 91

Mathematical statement

Exact Lean statement

lemma my_other_markov (hc : 0 ≤ c) (hε : 0 ≤ ε) (hg : ∀ a ∈ A, 0 ≤ g a)
    (h : ∑ a ∈ A, g a ≤ ε * c * #A) : (1 - ε) * #A ≤ #{a ∈ A | g a ≤ c}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma my_other_markov (hc : 0 ≤ c) (hε : 0 ≤ ε) (hg : ∀ a ∈ A, 0 ≤ g a)    (h : ∑ a ∈ A, g a ≤ ε * c * #A) : (1 - ε) * #A ≤ #{a ∈ A | g a ≤ c} := by  rcases hc.lt_or_eq with (hc | rfl)  · exact my_markov hc hg h  simp only [mul_zero, zero_mul] at h  classical  rw [one_sub_mul, sub_le_comm, ← cast_card_sdiff (filter_subset _ A), ← filter_not,    filter_false_of_mem]  · simp only [card_empty, CharP.cast_eq_zero]; positivity  intro i hi  rw [(sum_eq_zero_iff_of_nonneg hg).1 (h.antisymm (sum_nonneg hg)) i hi]  simp