carleson

Rationals are countable after conversion to reals, too. -/ private lemma Qᵣ_countable : Countable Qᵣ := propext Set.countable_coe_iff ▸ congr_arg Set.Countable Set.image_univ ▸ Set.countable_range Rat.cast

local notation "T" => carlesonOperatorReal K

lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (meas_f : AEStronglyMeasurable f) (hf : ∀ x, IntegrableOn f (Set.Ioo x (x + 2))) : Measurable (T f) := by wlog f_measurable : Measurable f · rcases meas_f with ⟨g, hg, hfg⟩ convert this (f := g) hg.aestronglyMeasurable _ hg.measurable using 1 · unfold carlesonOperatorReal congr with x congr with n congr with r congr with _ congr with _ congr 1 apply integral_congr_ae apply Filter.EventuallyEq.restrict filter_upwards [hfg] intro y hy congr intro x exact (integrableOn_congr_fun_ae hfg.restrict).mp (hf x) apply Measurable.iSup intro n set F : ℝ → ℝ → ℝ → ℂ := fun x r y ↦ {y | dist x y ∈ Set.Ioo r 1}.indicator (fun t ↦ f t * K x t * (Complex.I * ↑n * ↑t).exp) y with Fdef set G : ℝ → ℝ → ENNReal := fun x r ↦ ‖∫ (y : ℝ), F x r y‖ₑ with Gdef have hFG : (fun x ↦ ⨆ r, ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ₑ) = fun x ↦ ⨆ (r : ℝ) (_ : r ∈ Set.Ioo 0 1), G x r := by ext congr with r simp_rw [iSup_and', ← Set.mem_Ioo, Gdef, Fdef] congr rw [← integral_indicator annulus_measurableSet] rw [hFG] have hGr : (⨆ (r ∈ Set.Ioo 0 1), G · r) = (⨆ (r ∈ (Set.Ioo 0 1) ∩ Qᵣ), G · r) := by ext x rw [sup_eq_sup_dense_of_continuous Qᵣ isOpen_Ioo Qᵣ_dense] refine fun r ⟨hr, ⟩ ↦ (((EReal.continuous_coe_ennreal_iff.mp (EReal.continuous_coe_iff.mpr (continuous_iff_le_induced.mpr fun _ ↦ id))).continuousAt).comp (ContinuousAt.nnnorm ?) ).continuousWithinAt set S := Set.Ioo (r / 2) (2 * r) with Sdef set bound := fun y ↦ ‖F x (r / 2) y‖ with bound_def have h_bound : ∀ᶠ (s : ℝ) in nhds r, ∀ᵐ (a : ℝ), ‖F x s a‖ ≤ bound a := by rw [eventually_nhds_iff] use S constructor · intro s ⟨_, ⟩ apply Filter.Eventually.of_forall intro y rw [bound_def, Fdef, norm_indicator_eq_indicator_norm] simp only rw [norm_indicator_eq_indicator_norm] apply Set.indicator_le_indicator_of_subset · intro y ⟨, ⟩ constructor <;> linarith · intro y apply norm_nonneg constructor · apply isOpen_Ioo · rw [Sdef] constructor <;> linarith apply continuousAt_of_dominated _ h_bound · rw [bound_def, Fdef] conv => pattern ‖‖; rw [norm_indicator_eq_indicator_norm] rw [integrable_indicator_iff annulus_measurableSet] have bound_on_set : ∀ᵐ a ∂(volume.restrict {y | dist x y ∈ Set.Ioo (r / 2) 1}), ‖K x a * (Complex.I * (↑n * ↑a)).exp‖ ≤ ‖2 ^ (2 : ℝ) / (2 * (r / 2))‖ := by rw [ae_restrict_iff' annulus_measurableSet] filter_upwards with a ha rw [norm_mul, mul_comm Complex.I] norm_cast rw [Complex.norm_exp_ofReal_mul_I, mul_one] rw [Real.norm_eq_abs, abs_of_nonneg (by apply div_nonneg (by norm_num); linarith)] calc _ _ ≤ 2 ^ (2 : ℝ) / (2 * |x - a|) := Hilbert_kernel_bound _ ≤ 4 / (2 * (r / 2)) := by gcongr · linarith · rw [← Real.dist_eq] exact ha.1.le simp_rw [Complex.norm_mul] at bound_on_set simp_rw [Complex.norm_mul, mul_assoc] unfold IntegrableOn apply Integrable.mul_bdd _ (by fun_prop) (by simpa only [norm_mul, norm_norm]) apply Integrable.norm rw [annulus_real_eq (by linarith [hr]), ← IntegrableOn] apply IntegrableOn.mono_set (hf (x - 1)) intro y grind · have contOn1 : ∀ (y : ℝ), ContinuousOn (F x · y) (Set.Iio (dist x y)) := by intro y rw [continuousOn_iff_continuous_restrict] apply continuous_of_const simp only [Set.restrict_apply, Subtype.forall] intro s hs t ht rw [Fdef] simp only [Set.mem_Ioo] by_cases! h : dist x y < 1 · rw [Set.indicator_apply, ite_cond_eq_true, Set.indicator_apply, ite_cond_eq_true] · simpa using ⟨ht, h⟩ · simpa using ⟨hs, h⟩ · rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false] all_goals simpa using fun _ ↦ h have contOn2 : ∀ (y : ℝ), ContinuousOn (fun s ↦ F x s y) (Set.Ioi (min (dist x y) 1)) := by intro y rw [continuousOn_iff_continuous_restrict] apply continuous_of_const simp only [Set.restrict_apply, Subtype.forall] intro s hs t ht rw [Fdef] simp only [Set.mem_Ioo] rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false] · rw [Set.mem_Ioi, min_lt_iff] at ht simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt] intro h rcases ht with h' | h' · exfalso exact (lt_self_iff_false _).mp (h'.trans h) · exact (h'.trans h).le · rw [Set.mem_Ioi, min_lt_iff] at hs simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt] intro h rcases hs with h' | h' · exfalso exact (lt_self_iff_false _).mp (h'.trans h) · exact (h'.trans h).le have contOn : ∀ y, ∀ t ≠ dist x y, ContinuousAt (F x · y) t := by intro y t ht by_cases! h : t < dist x y · exact_mod_cast (contOn1 y).continuousAt (Iio_mem_nhds h) · exact ContinuousOn.continuousAt (contOn2 y) (Ioi_mem_nhds ((min_le_left _ _).trans_lt (lt_of_le_of_ne h ht.symm))) have subset_finite : {y | ¬ContinuousAt (F x · y) r} ⊆ ({x - r, x + r} : Finset ℝ) := by intro y hy have hxy : dist x y = r := by contrapose! hy rw [Set.mem_setOf_eq, not_not] exact contOn y r hy.symm rw [Real.dist_eq, abs_eq hr.le] at hxy simp only [Finset.coe_insert, Finset.coe_singleton, Set.mem_insert_iff, Set.mem_singleton_iff] cases hxy · left; linarith · right; linarith rw [ae_iff] exact measure_mono_null subset_finite (Finset.measure_zero _ ) · filter_upwards with r apply AEStronglyMeasurable.indicator _ annulus_measurableSet apply AEStronglyMeasurable.mul · apply AEStronglyMeasurable.mul meas_f (by fun_prop) · fun_prop rw [hGr] refine Measurable.biSup _ (Set.Countable.mono Set.inter_subset_right Qᵣ_countable) (fun r _ ↦ ?) apply measurable_coe_nnreal_ennreal.comp (measurable_nnnorm.comp _) rw [← stronglyMeasurable_iff_measurable] apply StronglyMeasurable.integral_prod_right rw [stronglyMeasurable_iff_measurable, Fdef] exact (measurable_mul_kernel f_measurable).indicator (measurable_dist measurableSet_Ioo)

--TODO: Refactor the measurability proof to use the following.

/- import Mathlib.MeasureTheory.Measure.MeasureSpace import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

open TopologicalSpace MeasureTheory Set

variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {ι : Type*} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [SecondCountableTopology ι] {f : ι → α → β} [ConditionallyCompleteLattice β] [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] [BorelSpace β]

-- lemma Measurable_iSup_gt {s : Set ι} [OrdConnected s] -- (h1f : ∀ x i, ContinuousWithinAt (f · x) s i) -- (h2f : ∀ i, Measurable (f i)) : -- Measurable (⨆ i ∈ s, f i ·) := by -- use SecondCountableTopology to rewrite the sup as a sup over the countable dense set (or similar) -- then use measurable_iSup