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

forest_operator'

Carleson.ForestOperator.Forests Β· Carleson/ForestOperator/Forests.lean:1068 to 1104

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.

Exact Lean statement

theorem forest_operator' {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⁻¹) *
    eLpNorm f 2 volume * (volume A) ^ (1/2 : ℝ)

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
theorem forest_operator' {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⁻¹) *    eLpNorm f 2 volume * (volume A) ^ (1/2 : ℝ) := by  /- This follows from the other version by taking for the test function `g` the argument of  the sum to be controlled. -/  have bf := bcs_of_measurable_of_le_indicator_f hf h2f  rw [← enorm_integral_starRingEnd_mul_eq_lintegral_enorm]; swap  Β· exact (BoundedCompactSupport.finset_sum (fun i hi ↦ by fun_prop)).integrable  rw [← integral_indicator hA]  simp_rw [indicator_mul_left, ← comp_def,    Set.indicator_comp_of_zero (g := starRingEnd β„‚) (by simp)]  have bAi (x : X) : β€–A.indicator (fun y ↦ (βˆ‘ u with u ∈ 𝔉, carlesonSum (𝔉 u) f y) /      β€–βˆ‘ u with u ∈ 𝔉, carlesonSum (𝔉 u) f yβ€–) xβ€– ≀ A.indicator 1 x := by    rw [norm_indicator_eq_indicator_norm]; apply indicator_le_indicator    rw [Complex.norm_div, norm_real, norm_norm, Pi.one_apply]    rcases eq_or_ne β€–βˆ‘ u with u ∈ 𝔉, carlesonSum (𝔉 u) f xβ€– 0 with hnorm | hnorm    Β· rw [hnorm]; norm_num    Β· rw [div_self hnorm]  apply (forest_operator 𝔉 hf h2f ?_ fun x ↦ ?_).trans; rotate_left  Β· exact Measurable.indicator (by fun_prop) hA  Β· exact (bAi _).trans (indicator_le_indicator_apply_of_subset sA (by simp))  gcongr  Β· simp only [sub_nonneg, inv_le_invβ‚€ zero_lt_two (q_pos X)]    exact (q_mem_Ioc (X := X)).2  Β· exact le_rfl  calc  _ ≀ eLpNorm (A.indicator (fun x ↦ 1) : X β†’ ℝ) 2 volume := by    apply eLpNorm_mono (fun x ↦ ?_)    simp only [indicator, coe_algebraMap, Real.norm_eq_abs]    split_ifs    Β· simpa using div_self_le_one _    Β· simp  _ ≀ _ := by    rw [eLpNorm_indicator_const hA (by norm_num) (by norm_num)]    simp