Source indexedlemma · leanprover/lean4:v4.32.0

layervol_eq_zero_of_lt

Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:405 to 414

Mathematical statement

Exact Lean statement

lemma layervol_eq_zero_of_lt {t : ℝ} (ht : (𝔐 (X := X) k n).toFinset.card < t) :
    layervol (X := X) k n t = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma layervol_eq_zero_of_lt {t : ℝ} (ht : (𝔐 (X := X) k n).toFinset.card < t) :    layervol (X := X) k n t = 0 := by  rw [layervol, measure_eq_zero_iff_ae_notMem]  refine ae_of_all volume fun x ↦ ?_; rw [mem_setOf, not_le]  calc    _ ≤ ((𝔐 (X := X) k n).toFinset.card : ℝ) := by      simp_rw [indicator_sum_eq_natCast, Nat.cast_le, indicator_apply, Pi.one_apply,        Finset.sum_boole, Nat.cast_id, filter_mem_univ_eq_toFinset]      exact Finset.card_le_card (Finset.filter_subset ..)    _ < _ := ht