Skip to main content
therefore
Sign inSign up
Open navigation
fpvandoorn/carleson
Source indexedlemma ยท leanprover/lean4:v4.32.0

TileStructure.Forest.sum_๐“™โ‚†_indicator_sq_eq

Carleson.ForestOperator.RemainingTiles ยท Carleson/ForestOperator/RemainingTiles.lean:369 to 382

Mathematical statement

Exact Lean statement

lemma sum_๐“™โ‚†_indicator_sq_eq {f : Grid X โ†’ X โ†’ โ„โ‰ฅ0โˆž} :
    (โˆ‘ J โˆˆ (๐“™โ‚† t uโ‚).toFinset, (J : Set X).indicator (f J) x) ^ 2 =
    โˆ‘ J โˆˆ (๐“™โ‚† t uโ‚).toFinset, (J : Set X).indicator (f J ยท ^ 2) x

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma sum_๐“™โ‚†_indicator_sq_eq {f : Grid X โ†’ X โ†’ โ„โ‰ฅ0โˆž} :    (โˆ‘ J โˆˆ (๐“™โ‚† t uโ‚).toFinset, (J : Set X).indicator (f J) x) ^ 2 =    โˆ‘ J โˆˆ (๐“™โ‚† t uโ‚).toFinset, (J : Set X).indicator (f J ยท ^ 2) x := by  rw [sq, Finset.sum_mul_sum, โ† Finset.sum_product']  have dsub : (๐“™โ‚† t uโ‚).toFinset.diag โŠ† (๐“™โ‚† t uโ‚).toFinset ร—หข (๐“™โ‚† t uโ‚).toFinset := by    rw [Finset.diag_eq_filter]    exact Finset.filter_subset ..  rw [โ† Finset.sum_subset dsub]; swap  ยท intro p mp np    simp_rw [Finset.mem_product, Finset.mem_diag, mem_toFinset, not_and] at mp np    specialize np mp.1    rw [โ† inter_indicator_mul, (pairwiseDisjoint_๐“™โ‚† mp.1 mp.2 np).inter_eq]    simp  simp_rw [Finset.sum_diag, โ† inter_indicator_mul, inter_self, โ† sq]