Source indexedtheorem · leanprover/lean4:v4.32.0

finitary_carleson

Carleson.FinitaryCarleson · Carleson/FinitaryCarleson.lean:110 to 124

Source documentation

Proposition 2.0.1

Exact Lean statement

theorem finitary_carleson : ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
    ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
    ∫⁻ x in G \ G', ‖∑ s ∈ Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * Q x y)‖ₑ ≤
    C2_0_1 a nnq * (volume G) ^ (1 - q⁻¹) * (volume F) ^ q⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem finitary_carleson : ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧    ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →    ∫⁻ x in G \ G', ‖∑ s ∈ Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * Q x y)‖ₑ ≤    C2_0_1 a nnq * (volume G) ^ (1 - q⁻¹) * (volume F) ^ q⁻¹ := by  have g : GridStructure X D κ S o := grid_existence X  have t : TileStructure Q D κ S o := tile_existence X  clear g  rcases discrete_carleson X with ⟨G', hG', h2G', hfG'⟩  refine ⟨G', hG', h2G', fun f meas_f h2f ↦ le_of_eq_of_le ?_ (hfG' f meas_f h2f)⟩  refine setLIntegral_congr_fun (measurableSet_G.diff hG') fun x hx ↦ ?_  simp_rw [carlesonSum, mem_univ, Finset.filter_true, tile_sum_operator hx, mul_sub, exp_sub,    mul_div, div_eq_mul_inv,    ← smul_eq_mul, integral_smul_const, ← Finset.sum_smul, _root_.enorm_smul]  suffices ‖(cexp (I • ((Q x) x : ℂ)))⁻¹‖ₑ = 1 by rw [this, mul_one]  simp [mul_comm I, enorm_eq_nnnorm]