Source indexedtheorem · leanprover/lean4:v4.32.0

enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:583 to 602

Mathematical statement

Exact Lean statement

theorem enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand
  {f g : X → ℂ} (hf : LocallyIntegrable f) (hg : LocallyIntegrable g)
  {θ : Θ X} {R₁ R₂ : ℝ} (R₁_pos : 0 < R₁) :
  ‖carlesonOperatorIntegrand K θ R₁ R₂ (f + g) x‖ₑ ≤
    ‖carlesonOperatorIntegrand K θ R₁ R₂ f x‖ₑ + ‖carlesonOperatorIntegrand K θ R₁ R₂ g x‖ₑ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand  {f g : X → ℂ} (hf : LocallyIntegrable f) (hg : LocallyIntegrable g)  {θ : Θ X} {R₁ R₂ : ℝ} (R₁_pos : 0 < R₁) :  ‖carlesonOperatorIntegrand K θ R₁ R₂ (f + g) x‖ₑ ≤    ‖carlesonOperatorIntegrand K θ R₁ R₂ f x‖ₑ + ‖carlesonOperatorIntegrand K θ R₁ R₂ g x‖ₑ := by  unfold carlesonOperatorIntegrand  apply le_trans _ (enorm_add_le _ _)  rw [← integral_add]  · apply le_of_eq    congr with y    simp only [Pi.add_apply]    ring  · apply integrableOn_coi_inner_annulus' _ R₁_pos    apply IntegrableOn.mono_set _ (Annulus.oo_subset_ball)    apply IntegrableOn.mono_set _ (ball_subset_closedBall)    apply hf.integrableOn_isCompact (isCompact_closedBall _ _)  · apply integrableOn_coi_inner_annulus' _ R₁_pos    apply IntegrableOn.mono_set _ (Annulus.oo_subset_ball)    apply IntegrableOn.mono_set _ (ball_subset_closedBall)    apply hg.integrableOn_isCompact (isCompact_closedBall _ _)