feat: Lemma 11.1.6 (#452)

I had to modify a little bit the blueprint, as it claimed an inequality
was always true, but I could only prove it in some range. If one writes
down the details of the proof, only this range is needed, so the global
strategy of proof works perfectly well modulo these minor adjustments.

I made the following Lean change: the `L^2` norm of `f` on an interval
`[a, b]` was used as `eLpNorm (indicator (Icc a b) f) 2` (where there is
a measure there, the volume, which is implicit). I changed it to
`eLpNorm f 2 (volume.restrict (Icc a b))` here and there, as this is how
we do integrals on sets and it is much more convenient to use since we
have a big API for restrictions of measures (and avoiding indicators is
always a good idea as they are pretty painful).

Author: sgouezel

Carleson/Classical/HilbertKernel.lean

@@ -1,4 +1,5 @@
 import Carleson.Classical.Basic
+import Mathlib.Data.Real.Pi.Bounds
 
 /- This file contains definitions and lemmas regarding the Hilbert kernel. -/
 
@@ -21,20 +22,21 @@ lemma k_of_one_le_abs {x : ℝ} (abs_le_one : 1 ≤ |x|) : k x = 0 := by
   rw [k, max_eq_right (by linarith)]
   simp
 
-@[measurability]
+@[fun_prop]
 lemma k_measurable : Measurable k := by
   unfold k
   fun_prop
 
-def K (x y : ℝ) : ℂ := k (x - y)
---TODO: maybe change to
---def K : ℝ → ℝ → ℂ := fun x y ↦ k (x - y)
+def K : ℝ → ℝ → ℂ := fun x y ↦ k (x - y)
+
+lemma K_def : K = fun x y ↦ k (x - y) := rfl
 
 lemma Hilbert_kernel_conj_symm {x y : ℝ} : K y x = conj (K x y) := by
   rw [K, ← neg_sub, k_of_neg_eq_conj_k, ← K]
 
-@[measurability]
-lemma Hilbert_kernel_measurable : Measurable (Function.uncurry K) := k_measurable.comp measurable_sub
+@[fun_prop]
+lemma Hilbert_kernel_measurable : Measurable (Function.uncurry K) :=
+  k_measurable.comp measurable_sub
 
 /- Lemma 11.1.11 (Hilbert kernel bound) -/
 lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := by
@@ -80,13 +82,15 @@ lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x
 
 /-Main part of the proof of Hilbert_kernel_regularity -/
 /-TODO: This can be local, i.e. invisible to other files. -/
-lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ 0 ≤ y') (ypos : 0 < y) (y2ley' : y / 2 ≤ y') (hy : y ≤ 1) (hy' : y' ≤ 1) :
+lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ 0 ≤ y') (ypos : 0 < y)
+    (y2ley' : y / 2 ≤ y') (hy : y ≤ 1) (hy' : y' ≤ 1) :
     ‖k (-y) - k (-y')‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by
   rw [k_of_abs_le_one, k_of_abs_le_one]
   · simp only [abs_neg, ofReal_neg, mul_neg]
     rw [_root_.abs_of_nonneg yy'nonneg.1, _root_.abs_of_nonneg yy'nonneg.2]
     set f : ℝ → ℂ := fun t ↦ (1 - t) / (1 - exp (-(I * t))) with hf
-    set f' : ℝ → ℂ := fun t ↦ (-1 + exp (-(I * t)) + I * (t - 1) * exp (-(I * t))) / (1 - exp (-(I * t))) ^ 2 with f'def
+    set f' : ℝ → ℂ := fun t ↦ (-1 + exp (-(I * t)) + I * (t - 1) * exp (-(I * t)))
+      / (1 - exp (-(I * t))) ^ 2 with f'def
     set c : ℝ → ℂ := fun t ↦ (1 - t) with cdef
     set c' : ℝ → ℂ := fun t ↦ -1 with c'def
     set d : ℝ → ℂ := fun t ↦ (1 - exp (-(I * t))) with ddef
@@ -235,7 +239,8 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} :
     have := this h_ y_y'_nonneg
     rw [y_def, y'_def] at this
     simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
-    rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
+    rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k,
+      ← abs_neg (y' - y)] at this
     simpa
   /-"Wlog" 0 < y-/
   by_cases ypos : y ≤ 0

Carleson/Classical/HilbertStrongType.lean

@@ -489,21 +489,17 @@ theorem eLpNorm_convolution_le_enorm_mul' [μ.IsAddRightInvariant] {p q r : ℝ
     ((L (f x)).le_opNorm (g y)).trans <| mul_le_mul_of_nonneg_right (L.le_opNorm _) (norm_nonneg _)
 
 open Set AddCircle in
-/-- **Young's convolution inequality** on (a, a + T]: the `L^r` seminorm of the convolution
-of `T`-periodic functions over (a, a + T] is bounded by `‖L‖ₑ` times the product of
-the `L^p` and `L^q` seminorms on that interval, where `1 / p + 1 / q = 1 / r + 1`. Here `‖L‖ₑ`
-is replaced with a  bound for `L` restricted to the ranges of `f` and `g`; see
-`eLpNorm_Ioc_convolution_le_enorm_mul` for a version using `‖L‖ₑ` explicitly. -/
-theorem eLpNorm_Ioc_convolution_le_of_norm_le_mul (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]
+lemma eLpNorm_Ioc_convolution_le_of_norm_le_mul_aux (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]
     {p q r : ℝ≥0∞} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
     {f : ℝ → E} {g : ℝ → E'} (hfT : f.Periodic T) (hgT : g.Periodic T)
     (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g)
     (c : ℝ) (hL : ∀ (x y : ℝ), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
-    eLpNorm ((Ioc a (a + T)).indicator fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r ≤
-    .ofReal c * eLpNorm ((Ioc a (a + T)).indicator f) p * eLpNorm ((Ioc a (a + T)).indicator g) q :=
+    eLpNorm (fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r (volume.restrict (Ioc a (a + T))) ≤
+    .ofReal c * eLpNorm f p (volume.restrict (Ioc a (a + T))) *
+      eLpNorm g q (volume.restrict (Ioc a (a + T))) :=
   calc
     _ = eLpNorm (liftIoc T a fun x ↦ ∫ (y : ℝ) in a..a + T, (L (f y)) (g (x - y))) r := by
-      rw [← eLpNorm_liftIoc T a]
+      rw [← eLpNorm_liftIoc' T a]
       · apply AEStronglyMeasurable.sub
         · apply AEStronglyMeasurable.integral_prod_right' (f := fun z ↦ L (f z.2) (g (z.1 - z.2)))
           apply L.aestronglyMeasurable_comp₂ hf.restrict.comp_snd
@@ -516,20 +512,62 @@ theorem eLpNorm_Ioc_convolution_le_of_norm_le_mul (a : ℝ) {T : ℝ} [hT : Fact
       exact eLpNorm_convolution_le_of_norm_le_mul' L hp hq hr hpqr (hf.liftIoc T a) (hg.liftIoc T a)
         c (by intros; apply hL)
     _ = _ := by
-      rw [← eLpNorm_liftIoc T a hf, ← eLpNorm_liftIoc T a hg]
+      rw [← eLpNorm_liftIoc' T a hf, ← eLpNorm_liftIoc' T a hg]
+
+open Set AddCircle in
+/-- **Young's convolution inequality** on (a, a + T]: the `L^r` seminorm of the convolution
+of `T`-periodic functions over (a, a + T] is bounded by `‖L‖ₑ` times the product of
+the `L^p` and `L^q` seminorms on that interval, where `1 / p + 1 / q = 1 / r + 1`. Here `‖L‖ₑ`
+is replaced with a bound for `L` restricted to the ranges of `f` and `g`; see
+`eLpNorm_Ioc_convolution_le_enorm_mul` for a version using `‖L‖ₑ` explicitly. -/
+theorem eLpNorm_Ioc_convolution_le_of_norm_le_mul (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]
+    {p q r : ℝ≥0∞} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
+    {f : ℝ → E} {g : ℝ → E'} (hgT : g.Periodic T)
+    (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g)
+    (c : ℝ) (hL : ∀ (x y : ℝ), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
+    eLpNorm (fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r (volume.restrict (Ioc a (a + T))) ≤
+    .ofReal c * eLpNorm f p (volume.restrict (Ioc a (a + T))) *
+      eLpNorm g q (volume.restrict (Ioc a (a + T))) := by
+  let f' := AddCircle.liftIoc T a f
+  let f'' := fun (x : ℝ) ↦ f' x
+  have hfT : f''.Periodic T := by simp [Function.Periodic, f'']
+  have : eLpNorm (fun x ↦ ∫ y in a..a+T, L (f'' y) (g (x - y))) r
+        (volume.restrict (Ioc a (a + T))) ≤
+      .ofReal c * eLpNorm f'' p (volume.restrict (Ioc a (a + T))) *
+      eLpNorm g q (volume.restrict (Ioc a (a + T))) := by
+    apply eLpNorm_Ioc_convolution_le_of_norm_le_mul_aux L a hp hq hr hpqr hfT hgT _ hg
+    · intro x y
+      simp only [liftIoc, Function.comp_apply, restrict_apply, f'', f']
+      apply hL
+    have A : AEStronglyMeasurable f'
+        (Measure.map (fun (x : ℝ) ↦ (x : AddCircle T)) (volume : Measure ℝ)) :=
+      AEStronglyMeasurable.mono_ac (quasiMeasurePreserving_coe_addCircle T).absolutelyContinuous
+        (by fun_prop)
+    exact A.comp_measurable (by fun_prop)
+  convert this using 3 with x
+  · rw [intervalIntegral.integral_of_le (by linarith [hT.out]),
+      intervalIntegral.integral_of_le (by linarith [hT.out])]
+    apply setIntegral_congr_fun measurableSet_Ioc (fun y hy ↦ ?_)
+    congr
+    exact (equivIoc_coe_of_mem a hy).symm
+  · apply eLpNorm_congr_ae
+    filter_upwards [self_mem_ae_restrict measurableSet_Ioc] with y hy
+    congr
+    exact (equivIoc_coe_of_mem a hy).symm
 
 open Set in
 /-- **Young's convolution inequality** on (a, a + T]: the `L^r` seminorm of the convolution
 of `T`-periodic functions over (a, a + T] is bounded by `‖L‖ₑ` times the product of
 the `L^p` and `L^q` seminorms on that interval, where `1 / p + 1 / q = 1 / r + 1`. -/
 theorem eLpNorm_Ioc_convolution_le_enorm_mul (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]
     {p q r : ℝ≥0∞} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
-    {f : ℝ → E} {g : ℝ → E'} (hfT : f.Periodic T) (hgT : g.Periodic T)
+    {f : ℝ → E} {g : ℝ → E'} (hgT : g.Periodic T)
     (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g) :
-    eLpNorm ((Ioc a (a + T)).indicator fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r ≤
-    ‖L‖ₑ * eLpNorm ((Ioc a (a + T)).indicator f) p * eLpNorm ((Ioc a (a + T)).indicator g) q := by
+    eLpNorm (fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r (volume.restrict (Ioc a (a + T))) ≤
+    ‖L‖ₑ * eLpNorm f p (volume.restrict (Ioc a (a + T)))
+      * eLpNorm g q (volume.restrict (Ioc a (a + T))) := by
   rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg L)]
-  exact eLpNorm_Ioc_convolution_le_of_norm_le_mul L a hp hq hr hpqr hfT hgT hf hg ‖L‖ <| fun x y ↦
+  exact eLpNorm_Ioc_convolution_le_of_norm_le_mul L a hp hq hr hpqr hgT hf hg ‖L‖ <| fun x y ↦
     ((L (f x)).le_opNorm (g y)).trans <| mul_le_mul_of_nonneg_right (L.le_opNorm _) (norm_nonneg _)
 
 end ENNReal

Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean

@@ -72,24 +72,46 @@ open AddCircle
 
 variable {E : Type*} (T a : ℝ) [hT : Fact (0 < T)] {f : ℝ → E}
 
-protected theorem AEStronglyMeasurable.liftIoc [TopologicalSpace E]
+@[fun_prop] protected theorem AEStronglyMeasurable.liftIoc [TopologicalSpace E]
     (hf : AEStronglyMeasurable f) : AEStronglyMeasurable (liftIoc T a f) :=
   (map_subtypeVal_map_equivIoc_volume T a ▸ hf.restrict).comp_measurable
     measurable_subtype_coe |>.comp_measurable (measurable_equivIoc T a)
 
-protected theorem AEStronglyMeasurable.liftIco [TopologicalSpace E]
+@[fun_prop] protected theorem AEStronglyMeasurable.liftIco [TopologicalSpace E]
     (hf : AEStronglyMeasurable f) : AEStronglyMeasurable (liftIco T a f) :=
   (hf.liftIoc T a).congr (liftIoc_ae_eq_liftIco f)
 
-protected theorem AEMeasurable.liftIoc [MeasurableSpace E] (hf : AEMeasurable f) :
+@[fun_prop] protected theorem AEMeasurable.liftIoc [MeasurableSpace E] (hf : AEMeasurable f) :
     AEMeasurable (liftIoc T a f) :=
   (map_subtypeVal_map_equivIoc_volume T a ▸ hf.restrict).comp_measurable
     measurable_subtype_coe |>.comp_measurable (measurable_equivIoc T a)
 
-protected theorem AEMeasurable.liftIco [MeasurableSpace E] (hf : AEMeasurable f) :
+@[fun_prop] protected theorem AEMeasurable.liftIco [MeasurableSpace E] (hf : AEMeasurable f) :
     AEMeasurable (liftIco T a f) :=
   (hf.liftIoc T a).congr (liftIoc_ae_eq_liftIco f)
 
+theorem map_coe_addCircle_volume_eq :
+    Measure.map (fun (x : ℝ) ↦ (x : AddCircle T)) volume =
+      (⊤ : ℝ≥0∞) • (volume : Measure (AddCircle T)) := by
+  have : (volume : Measure ℝ) =
+      Measure.sum (fun (n : ℤ) ↦ volume.restrict (Ioc (n • T) ((n + 1) • T))) := by
+    rw [← restrict_iUnion (Set.pairwise_disjoint_Ioc_zsmul T) (fun n ↦ measurableSet_Ioc),
+      iUnion_Ioc_zsmul hT.out, restrict_univ]
+  rw [this, Measure.map_sum (by fun_prop)]
+  have A (n : ℤ) : Measure.map (fun (x : ℝ) ↦ (x : AddCircle T))
+      (volume.restrict (Ioc (n • T) ((n + 1) • T)) ) = volume := by
+    simp only [zsmul_eq_mul, Int.cast_add, Int.cast_one, add_mul, one_mul]
+    exact (AddCircle.measurePreserving_mk T (n * T)).map_eq
+  simp only [A]
+  ext s hs
+  simp [hs]
+
+theorem quasiMeasurePreserving_coe_addCircle :
+    QuasiMeasurePreserving (fun (x : ℝ) ↦ (x : AddCircle T)) := by
+  refine ⟨by fun_prop, ?_⟩
+  rw [map_coe_addCircle_volume_eq]
+  exact smul_absolutelyContinuous
+
 end MeasureTheory
 
 
@@ -141,23 +163,45 @@ theorem eLpNorm_liftIoc (p : ℝ≥0∞) :
   rw [this, eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioc]
   exact (eLpNorm_comp_measurePreserving (hf.liftIoc T a) (AddCircle.measurePreserving_mk T a)).symm
 
+/-- The norm of the lift of a function `f` is equal to the norm of `f` on that period. -/
+theorem eLpNorm_liftIoc' (p : ℝ≥0∞) :
+    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm f p (volume.restrict ((Set.Ioc a (a + T)))) := by
+  rw [eLpNorm_liftIoc _ _ hf, eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioc]
+
 /-- The norm of the lift of a function `f` is equal to the norm of `f` on that period. -/
 theorem eLpNorm_liftIco (p : ℝ≥0∞) :
     eLpNorm (AddCircle.liftIco T a f) p = eLpNorm ((Set.Ico a (a + T)).indicator f) p := by
   rw [eLpNorm_congr_ae (liftIoc_ae_eq_liftIco f).symm, eLpNorm_liftIoc T a hf,
     eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ico,
     eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioc, restrict_Ico_eq_restrict_Ioc]
 
+/-- The norm of the lift of a function `f` is equal to the norm of `f` on that period. -/
+theorem eLpNorm_liftIco' (p : ℝ≥0∞) :
+    eLpNorm (AddCircle.liftIco T a f) p = eLpNorm f p (volume.restrict (Set.Ico a (a + T))) := by
+  rw [eLpNorm_liftIco _ _ hf, eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ico]
+
 /-- The norm of the lift of a periodic function `f` is equal to the norm of `f` on any period. -/
 theorem eLpNorm_liftIoc_of_periodic (hfT : Periodic f T) (p : ℝ≥0∞) :
     eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm ((Set.Ioc a' (a' + T)).indicator f) p := by
   rw [liftIoc_eq_liftIoc a a' hfT, eLpNorm_liftIoc T a' hf p]
 
+/-- The norm of the lift of a periodic function `f` is equal to the norm of `f` on any period. -/
+theorem eLpNorm_liftIoc_of_periodic' (hfT : Periodic f T) (p : ℝ≥0∞) :
+    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm f p (volume.restrict (Set.Ioc a' (a' + T))) := by
+  rw [eLpNorm_liftIoc_of_periodic T a a' hf hfT,
+    eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioc]
+
 /-- The norm of the lift of a periodic function `f` is equal to the norm of `f` on any period. -/
 theorem eLpNorm_liftIco_of_periodic (hfT : Periodic f T) (p : ℝ≥0∞) :
     eLpNorm (AddCircle.liftIco T a f) p = eLpNorm ((Set.Ico a' (a' + T)).indicator f) p := by
   rw [liftIco_eq_liftIco a a' hfT, eLpNorm_liftIco T a' hf p]
 
+/-- The norm of the lift of a periodic function `f` is equal to the norm of `f` on any period. -/
+theorem eLpNorm_liftIco_of_periodic' (hfT : Periodic f T) (p : ℝ≥0∞) :
+    eLpNorm (AddCircle.liftIco T a f) p = eLpNorm f p (volume.restrict (Set.Ico a' (a' + T))) := by
+  rw [eLpNorm_liftIco_of_periodic T a a' hf hfT,
+    eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ico]
+
 end eLpNorm
 
 end AddCircle

Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean

@@ -67,7 +67,7 @@ end Periodic
 
 /-- Ioc version of mathlib `coe_eq_coe_iff_of_mem_Ico` -/
 lemma coe_eq_coe_iff_of_mem_Ioc {p : 𝕜} [hp : Fact (0 < p)]
-    {a : 𝕜} [Archimedean 𝕜] {x y : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) (hy : y ∈ Set.Ioc a (a + p)) : 
+    {a : 𝕜} [Archimedean 𝕜] {x y : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) (hy : y ∈ Set.Ioc a (a + p)) :
     (x : AddCircle p) = y ↔ x = y := by
   refine ⟨fun h => ?_, by tauto⟩
   suffices (⟨x, hx⟩ : Set.Ioc a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
@@ -82,5 +82,14 @@ lemma eq_coe_Ioc {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜]
   exact ⟨b.1, by simpa only [zero_add] using b.2,
     (QuotientAddGroup.equivIocMod hp.out 0).symm_apply_apply a⟩
 
+lemma coe_equivIoc {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] (a : 𝕜) {y : AddCircle p} :
+    (equivIoc p a y : AddCircle p) = y :=
+  (equivIoc p a).left_inv y
+
+lemma equivIoc_coe_of_mem {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] (a : 𝕜) {y : 𝕜}
+    (hy : y ∈ Set.Ioc a (a + p)) :
+    equivIoc p a y = y := by
+  have : equivIoc p a y = ⟨y, hy⟩ := (equivIoc p a).right_inv ⟨y, hy⟩
+  simp [this]
 
 end AddCircle

Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean

@@ -25,7 +25,7 @@ lemma memLp_top_K_on_ball_complement (hr : 0 < r) {x : X}:
       · intro y hy
         apply enorm_K_le_ball_complement' hr hy
 
-lemma czoperator_bound {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (x : X) :
+lemma czOperator_bound {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (x : X) :
     ∃ (M : ℝ≥0), ∀ᵐ y ∂(volume.restrict (ball x r)ᶜ), ‖K x y * g y‖ ≤ M := by
   let M0 := (C_K a / volume (ball x r) * eLpNorm g ∞).toNNReal
   use M0
@@ -62,28 +62,38 @@ lemma czoperator_bound {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r
     · exact measurableSet_ball.compl.nullMeasurableSet
   · exact measurableSet_ball.compl.nullMeasurableSet
 
+omit [IsOneSidedKernel a K] in
 @[fun_prop]
-lemma czOperator_aestronglyMeasurable' {g : X → ℂ} (hg : AEStronglyMeasurable g) :
+lemma czOperator_aestronglyMeasurable' (hK : Measurable (uncurry K))
+    {g : X → ℂ} (hg : AEStronglyMeasurable g) :
     AEStronglyMeasurable (fun x ↦ czOperator K r g x) := by
   unfold czOperator
   conv => arg 1; intro x; rw [← integral_indicator (by measurability)]
   let f := fun (x,z) ↦ (ball x r)ᶜ.indicator (fun y ↦ K x y * g y) z
   apply AEStronglyMeasurable.integral_prod_right' (f := f)
   unfold f
   apply AEStronglyMeasurable.indicator
-  · apply Continuous.comp_aestronglyMeasurable₂ (by fun_prop) aestronglyMeasurable_K
+  · apply Continuous.comp_aestronglyMeasurable₂ (by fun_prop) hK.aestronglyMeasurable
     exact hg.comp_snd
   · conv => arg 1; change {x : (X × X) | x.2 ∈ (ball x.1 r)ᶜ}
     simp_rw [mem_compl_iff, mem_ball, not_lt]
     apply measurableSet_le <;> fun_prop
 
 @[fun_prop]
--- TODO: remove in favour of `czOperator_aestronglyMeasurable'` (and unprime that one)
-lemma czOperator_aestronglyMeasurable {g : X → ℂ} (hg : BoundedFiniteSupport g) :
+lemma czOperator_aestronglyMeasurable
+    {g : X → ℂ} (hg : AEStronglyMeasurable g) :
     AEStronglyMeasurable (fun x ↦ czOperator K r g x) :=
-  czOperator_aestronglyMeasurable' hg.aestronglyMeasurable
+  czOperator_aestronglyMeasurable' measurable_K hg
 
-lemma czoperator_welldefined {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (x : X):
+/- Next lemma is useful for fun_prop in a context where it can not find the relevant measure to
+apply `czOperator_aestronglyMeasurable`.
+TODO: investigate -/
+@[fun_prop]
+lemma czOperator_aestronglyMeasurable_aux {g : X → ℂ} (hg : BoundedFiniteSupport g) :
+    AEStronglyMeasurable (fun x ↦ czOperator K r g x) :=
+  czOperator_aestronglyMeasurable hg.aestronglyMeasurable
+
+lemma czOperator_welldefined {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (x : X):
     IntegrableOn (fun y => K x y * g y) (ball x r)ᶜ volume := by
   let Kxg := fun y ↦ K x y * g y
   have mKxg : AEStronglyMeasurable Kxg := by
@@ -99,7 +109,7 @@ lemma czoperator_welldefined {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr :
     simp only [NNReal.zero_le_coe]
 
   have bdd_Kxg : ∃ (M : ℝ), ∀ᵐ y ∂(volume.restrict ((ball x r)ᶜ ∩ support Kxg)), ‖Kxg y‖ ≤ M := by
-    obtain ⟨M, hM⟩ := czoperator_bound (K := K) hg hr x
+    obtain ⟨M, hM⟩ := czOperator_bound (K := K) hg hr x
     use M
     rw [ae_iff, Measure.restrict_apply₀']
     · conv =>
@@ -129,12 +139,12 @@ lemma czoperator_welldefined {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr :
   · exact hM
 
 -- This could be adapted to state T_r is a linear operator but maybe it's not worth the effort
-lemma czoperator_sub {f g : X → ℂ} (hf : BoundedFiniteSupport f) (hg : BoundedFiniteSupport g) (hr : 0 < r) :
+lemma czOperator_sub {f g : X → ℂ} (hf : BoundedFiniteSupport f) (hg : BoundedFiniteSupport g) (hr : 0 < r) :
     czOperator K r (f - g) = czOperator K r f - czOperator K r g := by
   ext x
   unfold czOperator
   simp_rw [Pi.sub_apply, mul_sub_left_distrib,
-    integral_sub (czoperator_welldefined hf hr x) (czoperator_welldefined hg hr x)]
+    integral_sub (czOperator_welldefined hf hr x) (czOperator_welldefined hg hr x)]
 
 /-- Lemma 10.1.1 -/
 lemma geometric_series_estimate {x : ℝ} (hx : 2 ≤ x) :