Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.BoundedCompactSupport.carlesonOn

Carleson.Operators · Carleson/Operators.lean:144 to 155

Mathematical statement

Exact Lean statement

@[fun_prop]
theorem BoundedCompactSupport.carlesonOn {f : X → ℂ}
    (hf : BoundedCompactSupport f) : BoundedCompactSupport (carlesonOn p f) where
  memLp_top

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[fun_prop]theorem BoundedCompactSupport.carlesonOn {f : X → ℂ}    (hf : BoundedCompactSupport f) : BoundedCompactSupport (carlesonOn p f) where  memLp_top := by    obtain ⟨C, hC⟩ := bddAbove_def.mp <| hf.bddAbove_norm_carlesonOn p    simp_rw [mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hC    exact memLp_top_of_bound hf.aestronglyMeasurable.carlesonOn C (.of_forall hC)  hasCompactSupport := by    suffices support (_root_.carlesonOn p f) ⊆ 𝓘 p by      refine HasCompactSupport.of_support_subset_isBounded ?_ this      exact Metric.isBounded_ball.subset Grid_subset_ball    exact support_carlesonOn_subset_E.trans E_subset_𝓘