Source indexedlemma · leanprover/lean4:v4.32.0

carlesonSum_𝔓₁_eq_sum

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:692 to 711

Source documentation

From the fact that the ℭ₅ k n j are disjoint, one can rewrite the whole Carleson sum over 𝔓₁ (the union of the ℭ₅ k n j) as a sum of Carleson sums over the ℭ₅ k n j.

Exact Lean statement

lemma carlesonSum_𝔓₁_eq_sum {f : X → ℂ} {x : X} :
    carlesonSum 𝔓₁ f x = ∑ n ≤ maxℭ X, ∑ k ≤ n, ∑ j ≤ 2 * n + 3, carlesonSum (ℭ₅ k n j) f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma carlesonSum_𝔓₁_eq_sum {f : X → ℂ} {x : X} :    carlesonSum 𝔓₁ f x = ∑ n ≤ maxℭ X, ∑ k ≤ n, ∑ j ≤ 2 * n + 3, carlesonSum (ℭ₅ k n j) f x := by  simp only [Finset.sum_sigma']  rw [sum_carlesonSum_of_pairwiseDisjoint]; swap  · rintro ⟨n, k, j⟩ - ⟨n', k', j'⟩ - h    simp only [ne_eq, Sigma.mk.inj_iff, heq_eq_eq] at h    simp only [Function.onFun]    have W := pairwiseDisjoint_ℭ₅ (X := X) (mem_univ ⟨k, n, j⟩) (mem_univ ⟨k', n', j'⟩)      (by simp [-not_and]; tauto)    simpa [Function.onFun, disjoint_left] using W  congr  ext p  simp only [𝔓₁, mem_iUnion, exists_prop, Finset.mem_sigma, Finset.mem_Iic, Sigma.exists]  constructor  · rintro ⟨n, k, hk, j, hj, hp⟩    refine ⟨n, k, j, ⟨?_, hk, hj⟩, hp⟩    have : (ℭ (X := X) k n).Nonempty := ⟨p, ℭ₅_subset_ℭ hp⟩    exact le_maxℭ_of_nonempty this  · rintro ⟨n, k, j, ⟨hn, hk, hj⟩, hp⟩    exact ⟨n, k, hk, j, hj, hp⟩