Skip to main content
therefore
Sign inSign up
Open navigation
fpvandoorn/carleson
Source indexedtheorem Β· leanprover/lean4:v4.32.0

forest_operator_le_volume

Carleson.ForestOperator.Forests Β· Carleson/ForestOperator/Forests.lean:1110 to 1122

Source documentation

Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function, and with the upper bound in terms of volume F and volume G.

Exact Lean statement

theorem forest_operator_le_volume {n : β„•} (𝔉 : Forest X n) {f : X β†’ β„‚} {A : Set X}
    (hf : Measurable f) (h2f : βˆ€ x, β€–f xβ€– ≀ F.indicator 1 x) (hA : MeasurableSet A) (sA : A βŠ† G) :
    ∫⁻ x in A, β€–βˆ‘ u with u ∈ 𝔉, carlesonSum (𝔉 u) f xβ€–β‚‘ ≀
    C2_0_4 a q n * (densβ‚‚ (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *
    (volume F) ^ (1/2 : ℝ) * (volume A) ^ (1/2 : ℝ)

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
theorem forest_operator_le_volume {n : β„•} (𝔉 : Forest X n) {f : X β†’ β„‚} {A : Set X}    (hf : Measurable f) (h2f : βˆ€ x, β€–f xβ€– ≀ F.indicator 1 x) (hA : MeasurableSet A) (sA : A βŠ† G) :    ∫⁻ x in A, β€–βˆ‘ u with u ∈ 𝔉, carlesonSum (𝔉 u) f xβ€–β‚‘ ≀    C2_0_4 a q n * (densβ‚‚ (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *    (volume F) ^ (1/2 : ℝ) * (volume A) ^ (1/2 : ℝ) := by  apply (forest_operator' 𝔉 hf h2f hA sA).trans  gcongr  calc  _ ≀ eLpNorm (F.indicator (fun x ↦ 1) : X β†’ ℝ) 2 volume :=    eLpNorm_mono (fun x ↦ (h2f x).trans (le_abs_self _))  _ ≀ _ := by    rw [eLpNorm_indicator_const measurableSet_F (by norm_num) (by norm_num)]    simp