Source indexedlemma · leanprover/lean4:v4.32.0

adjointCarlesonSum_adjoint

Carleson.Operators · Carleson/Operators.lean:406 to 418

Source documentation

adjointCarlesonSum is the adjoint of carlesonSum.

Exact Lean statement

lemma adjointCarlesonSum_adjoint
    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (ℭ : Set (𝔓 X)) :
    ∫ x, conj (g x) * carlesonSum ℭ f x = ∫ x, conj (adjointCarlesonSum ℭ g x) * f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma adjointCarlesonSum_adjoint    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (ℭ : Set (𝔓 X)) :    ∫ x, conj (g x) * carlesonSum ℭ f x = ∫ x, conj (adjointCarlesonSum ℭ g x) * f x := by  unfold carlesonSum  simp_rw [Finset.mul_sum]  classical calc    _ = ∑ p with p ∈ ℭ, ∫ x, conj (g x) * carlesonOn p f x :=      integral_finsetSum _ fun p _ ↦ by fun_prop    _ = ∑ p with p ∈ ℭ, ∫ y, conj (adjointCarleson p g y) * f y := by      simp_rw [adjointCarleson_adjoint hf hg]    _ = ∫ y, ∑ p with p ∈ ℭ, conj (adjointCarleson p g y) * f y :=      (integral_finsetSum _ fun p _ ↦ by fun_prop).symm    _ = _ := by congr!; rw [← Finset.sum_mul, ← map_sum]; rfl