fpvandoorn/carleson
Source indexedtheorem · leanprover/lean4:v4.32.0
antichain_operator_le_volume
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:464 to 476
Source documentation
Version of the antichain 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 antichain_operator_le_volume {A : Set X} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
(hf : Measurable f) (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : A ⊆ G) :
∫⁻ x in A, ‖carlesonSum 𝔄 f x‖ₑ ≤
C2_0_3 a nnq * dens₁ 𝔄 ^ ((q - 1) / (8 * a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *
volume F ^ (1/2 : ℝ) * volume G ^ (1/2 : ℝ)Complete declaration
Lean source
Full Lean sourceLean 4
theorem antichain_operator_le_volume {A : Set X} (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (hf : Measurable f) (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : A ⊆ G) : ∫⁻ x in A, ‖carlesonSum 𝔄 f x‖ₑ ≤ C2_0_3 a nnq * dens₁ 𝔄 ^ ((q - 1) / (8 * a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) * volume F ^ (1/2 : ℝ) * volume G ^ (1/2 : ℝ) := by apply (antichain_operator' h𝔄 hf hfF hA).trans gcongr calc _ ≤ eLpNorm (F.indicator (fun x ↦ 1) : X → ℝ) 2 volume := eLpNorm_mono (fun x ↦ (hfF x).trans (le_abs_self _)) _ ≤ _ := by rw [eLpNorm_indicator_const measurableSet_F (by norm_num) (by norm_num)] simp