Source indexedtheorem · leanprover/lean4:v4.32.0

linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:605 to 619

Mathematical statement

Exact Lean statement

theorem linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator
  {f g : X → ℂ} (hf : LocallyIntegrable f) (hg : LocallyIntegrable g) {θ : Θ X} :
  linearizedCarlesonOperator (fun _ ↦ θ) K (f + g) x ≤
    linearizedCarlesonOperator (fun _ ↦ θ) K f x + linearizedCarlesonOperator (fun _ ↦ θ) K g x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator  {f g : X → ℂ} (hf : LocallyIntegrable f) (hg : LocallyIntegrable g) {θ : Θ X} :  linearizedCarlesonOperator (fun _ ↦ θ) K (f + g) x ≤    linearizedCarlesonOperator (fun _ ↦ θ) K f x + linearizedCarlesonOperator (fun _ ↦ θ) K g x := by  unfold linearizedCarlesonOperator  apply le_trans _ (iSup_add_le _ _)  gcongr with R₁  apply le_trans _ (iSup_add_le _ _)  gcongr with R₂  apply le_trans _ (iSup_add_le _ _)  gcongr with R₁_pos  apply le_trans _ (iSup_add_le _ _)  gcongr with R₁_lt_R₂  simp only  apply enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand hf hg R₁_pos