Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.S_eq_zero_of_topCube_mem_𝓙₀

Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:66 to 77

Mathematical statement

Exact Lean statement

lemma S_eq_zero_of_topCube_mem_𝓙₀ {𝔖 : Set (𝔓 X)} (h𝔖 : 𝔖.Nonempty) (h : topCube ∈ 𝓙₀ 𝔖) :
    S = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma S_eq_zero_of_topCube_mem_𝓙₀ {𝔖 : Set (𝔓 X)} (h𝔖 : 𝔖.Nonempty) (h : topCube ∈ 𝓙₀ 𝔖) :    S = 0 := by  suffices (S : ℤ) = -(S : ℤ) by exact_mod_cast eq_zero_of_neg_eq this.symm  rw [𝓙₀, mem_setOf_eq, s, s_topCube] at h  apply h.resolve_right  push Not  have ⟨p, hp⟩ := h𝔖  refine ⟨p, hp, subset_topCube.trans <| Grid_subset_ball.trans <| ball_subset_ball ?_⟩  gcongr  · norm_num  · exact one_le_realD _  · exact scale_mem_Icc.2.trans (Int.le.intro 1 rfl)