Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.sum_χ

Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:237 to 246

Source documentation

Part of Lemma 7.5.2.

Exact Lean statement

lemma sum_χ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (x : X) :
    ∑ J ∈ 𝓙₅ t u₁ u₂, χ t u₁ u₂ J x = (𝓘 u₁ : Set X).indicator 1 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_χ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (x : X) :    ∑ J ∈ 𝓙₅ t u₁ u₂, χ t u₁ u₂ J x = (𝓘 u₁ : Set X).indicator 1 x := by  simp_rw [χ, ← Finset.sum_div, NNReal.div_self_eq_ite, indicator, Pi.one_apply]  refine if_congr ?_ rfl rfl  simp_rw [Finset.sum_pos_iff, mem_toFinset, χtilde_pos_iff]  conv_lhs => enter [1, J]; rw [and_rotate]  rw [exists_and_left, Grid.mem_def, and_iff_left_iff_imp, ← union_𝓙₅ hu₁ hu₂ hu h2u]; intro mx  rw [mem_iUnion₂] at mx; obtain ⟨J, mJ, hJ⟩ := mx  refine ⟨J, Grid_subset_ball.trans (ball_subset_ball ?_) hJ, mJ⟩  change (4 : ℝ) * D ^ s J ≤ _; gcongr; norm_num