Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.adjoint_tile_support2_sum

Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:63 to 73

Mathematical statement

Exact Lean statement

lemma adjoint_tile_support2_sum (hu : u ∈ t) :
    adjointCarlesonSum (t u) f =
    (𝓘 u : Set X).indicator (adjointCarlesonSum (t u) ((𝓘 u : Set X).indicator f))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma adjoint_tile_support2_sum (hu : u ∈ t) :    adjointCarlesonSum (t u) f =    (𝓘 u : Set X).indicator (adjointCarlesonSum (t u) ((𝓘 u : Set X).indicator f)) := by  unfold adjointCarlesonSum  classical  calc    _ = ∑ p with p ∈ t u,        (𝓘 u : Set X).indicator (adjointCarleson p ((𝓘 u : Set X).indicator f)) := by      ext x; simp only [Finset.sum_apply]; congr! 1 with p mp      rw [Finset.mem_filter_univ] at mp; rw [adjoint_tile_support2 hu mp]    _ = _ := by simp_rw [← Finset.indicator_sum, ← Finset.sum_apply]