Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.e728_push_toReal

Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:463 to 474

Mathematical statement

Exact Lean statement

lemma e728_push_toReal (hf : BoundedCompactSupport f) :
    (t.boundaryOperator u f x).toReal = ∑ I : Grid X,
      (I : Set X).indicator (fun _ ↦ ∑ J ∈ 𝓙' t u (c I) (s I), (ijIntegral f I J).toReal) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma e728_push_toReal (hf : BoundedCompactSupport f) :    (t.boundaryOperator u f x).toReal = ∑ I : Grid X,      (I : Set X).indicator (fun _ ↦ ∑ J ∈ 𝓙' t u (c I) (s I), (ijIntegral f I J).toReal) x := by  rw [boundaryOperator, ENNReal.toReal_sum]  · congr! with I -    unfold indicator; split_ifs    · exact ENNReal.toReal_sum fun _ _ ↦ (ijIntegral_lt_top hf).ne    · rfl  · have bof := fun x ↦ boundaryOperator_lt_top hf (t := t) (u := u) (x := x)    unfold boundaryOperator at bof    simp_rw [ENNReal.sum_lt_top] at bof    exact fun I mI ↦ (bof x I mI).ne