Source indexedlemma · leanprover/lean4:v4.32.0

my_markov

APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:68 to 78

Mathematical statement

Exact Lean statement

lemma my_markov (hc : 0 < c) (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_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a ∈ A, g a ≤ ε * c * #A) :    (1 - ε) * #A ≤ #{a ∈ A | g a ≤ c} := by  classical  have := h.trans'    (sum_le_sum_of_subset_of_nonneg (filter_subset (¬g · ≤ c) A) fun i hi _ ↦ hg _ hi)  have :=    (card_nsmul_le_sum _ _ c (by simp +contextual [le_of_lt])).trans this  rw [nsmul_eq_mul, mul_right_comm] at this  have := le_of_mul_le_mul_right this hc  rw [filter_not, cast_card_sdiff (filter_subset _ _)] at this  linarith only [this]