Source indexedlemma · leanprover/lean4:v4.32.0

forest_disjoint

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:313 to 327

Source documentation

This one could deserve a lemma in the blueprint, as it is needed to decompose the sum of Carleson operators over disjoint subfamilies.

Exact Lean statement

lemma forest_disjoint : (𝔘₃ k n j).PairwiseDisjoint (fun u ↦ 𝔗₂ (X := X) k n j u)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma forest_disjoint : (𝔘₃ k n j).PairwiseDisjoint (fun u ↦ 𝔗₂ (X := X) k n j u) := by  intro u hu u' hu' huu'  simp only [Function.onFun]  apply disjoint_left.2 (fun p pu pu' ↦ huu' ?_)  simp only [𝔗₂, mem_inter_iff, mem_iUnion, exists_prop] at pu pu'  rcases pu.2 with ⟨v, v_mem, v_rel, pv⟩  rcases pu'.2 with ⟨v', v'_mem, v'_rel, pv'⟩  have E : URel k n j v v' :=    Or.inr ⟨p, pv, smul_mono pv'.2.2 le_rfl (by norm_num)⟩  have : URel k n j u v' :=    (equivalenceOn_urel (X := X)).trans (𝔘₃_subset_𝔘₂ hu) v_mem v'_mem v_rel E  have : URel k n j u u' := by    apply (equivalenceOn_urel (X := X)).trans (𝔘₃_subset_𝔘₂ hu) v'_mem (𝔘₃_subset_𝔘₂ hu') this    exact (equivalenceOn_urel (X := X)).symm (𝔘₃_subset_𝔘₂ hu') v'_mem v'_rel  exact (equivalenceOn_urel (X := X)).reprs_inj hu hu' this