Bump to v4.18.0 (#279)

Ruben-VandeVelde · pitmonticone · web-flow · commit 841c1e834397 · 2025-04-01T19:09:10.000+02:00
Co-authored-by: Pietro Monticone &lt;38562595+pitmonticone@users.noreply.github.com&gt;
diff --git a/Carleson.lean b/Carleson.lean
@@ -48,7 +48,6 @@ import Carleson.ToMathlib.ENorm
 import Carleson.ToMathlib.HardyLittlewood
 import Carleson.ToMathlib.MeasureReal
 import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic
-import Carleson.ToMathlib.MeasureTheory.Group.LIntegral
 import Carleson.ToMathlib.MeasureTheory.Integral.Lebesgue
 import Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities
 import Carleson.ToMathlib.MeasureTheory.Integral.Periodic
diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean
@@ -525,8 +525,8 @@ lemma carlesonOperatorReal_le_carlesonOperator : T ≤ carlesonOperator K := by
 lemma rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G)
     (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
     ∫⁻ x in G, T f x ≤ C10_0_1 4 2 * (volume G) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹ := by
-  have conj_exponents : NNReal.IsConjExponent 2 2 := by
-    rw [NNReal.isConjExponent_iff_eq_conjExponent]
+  have conj_exponents : NNReal.HolderConjugate 2 2 := by
+    rw [NNReal.holderConjugate_iff_eq_conjExponent]
     · ext; norm_num
     norm_num
   calc ∫⁻ x in G, T f x
diff --git a/Carleson/ForestOperator/L2Estimate.lean b/Carleson/ForestOperator/L2Estimate.lean
@@ -660,7 +660,7 @@ lemma boundary_operator_bound_aux (hf : BoundedCompactSupport f) (hg : BoundedCo
       gcongr; exact setLIntegral_le_lintegral _ _
     _ ≤ 2 ^ (9 * a + 1) * eLpNorm f 2 volume * eLpNorm (MB volume 𝓑 c𝓑 r𝓑 g) 2 volume := by
       rw [mul_assoc]; gcongr
-      exact ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm ⟨ENNReal.inv_two_add_inv_two⟩
+      exact ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm ⟨by simpa using ENNReal.inv_two_add_inv_two⟩
         hf.aestronglyMeasurable.aemeasurable.enorm
         (AEStronglyMeasurable.maximalFunction 𝓑.to_countable).aemeasurable
     _ ≤ 2 ^ (9 * a + 1) * eLpNorm f 2 volume * (2 ^ (a + (3 / 2 : ℝ)) * eLpNorm g 2 volume) := by
@@ -890,7 +890,7 @@ lemma tree_projection_estimate
       nth_rewrite 2 [← setLIntegral_univ]
       exact lintegral_mono_set (fun _ _ ↦ trivial)
     _ ≤ eLpNorm eaOC 2 volume * eLpNorm (cS_bound t u f) 2 volume := by
-      have isConj : Real.IsConjExponent 2 2 := by constructor <;> norm_num
+      have isConj : Real.HolderConjugate 2 2 := by constructor <;> norm_num
       have : AEMeasurable eaOC := (stronglyMeasurable_approxOnCube _ _).aemeasurable.ennreal_ofReal
       convert ENNReal.lintegral_mul_le_Lp_mul_Lq volume isConj this aeMeasurable_cS_bound <;>
         simp [eLpNorm, eLpNorm']
diff --git a/Carleson/ForestOperator/PointwiseEstimate.lean b/Carleson/ForestOperator/PointwiseEstimate.lean
@@ -436,7 +436,8 @@ private lemma sum_pow_two_le (a b : ℤ) : ∑ s ∈ Finset.Icc a b, (2 : ℝ≥
     linarith
   · intro n hn m hm hnm
     rw [Finset.mem_Icc] at hn hm
-    simpa [Int.sub_nonneg.mpr hn.1, Int.sub_nonneg.mpr hm.1] using congrArg Int.ofNat hnm
+    have := congrArg Int.ofNat hnm
+    simpa [max_eq_left (Int.sub_nonneg.mpr hn.1), max_eq_left (Int.sub_nonneg.mpr hm.1)] using this
   · exact fun n hn ↦ by use a + n, by simp [Nat.le_of_lt_succ (Finset.mem_range.mp hn)], by simp
   · intro n hn
     rw [← zpow_natCast, Int.ofNat_toNat, ← zpow_add' (Or.inl two_ne_zero),
diff --git a/Carleson/ForestOperator/QuantativeEstimate.lean b/Carleson/ForestOperator/QuantativeEstimate.lean
@@ -347,7 +347,7 @@ private lemma eLpNorm_approxOnCube_two_le {C : Set (Grid X)}
           volume (J : Set X) := by
       refine Finset.sum_le_sum fun J hJ ↦ ENNReal.div_le_div_right (pow_le_pow_left' ?_ 2) _
       simpa using ENNReal.lintegral_mul_le_Lp_mul_Lq (f := (‖f ·‖ₑ)) (g := 1)
-        (volume.restrict (J ∩ s)) ((Real.isConjExponent_iff 2 2).mpr (by norm_num))
+        (volume.restrict (J ∩ s)) ((Real.holderConjugate_iff (p := 2) (q := 2)).mpr (by norm_num))
         hf.stronglyMeasurable.aemeasurable.enorm measurable_const.aemeasurable
     _ = ∑ J ∈ Finset.univ.filter (· ∈ C), (∫⁻ y in J ∩ s, ‖f y‖ₑ ^ 2) ^ (1 / (2 : ℝ) * 2) *
           volume (J ∩ s) ^ (1 / (2 : ℝ) * 2) / volume (J : Set X) := by
diff --git a/Carleson/LinearizedMetricCarleson.lean b/Carleson/LinearizedMetricCarleson.lean
@@ -19,7 +19,7 @@ variable {K : X → X → ℂ}
 /- Theorem 1.0.3 -/
 theorem linearized_metric_carleson [CompatibleFunctions ℝ X (defaultA a)]
   [IsCancellative X (defaultτ a)] [IsOneSidedKernel a K]
-    (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
+    (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
     (Q : SimpleFunc X (Θ X)) {θ : Θ X}
     (hF : MeasurableSet F) (hG : MeasurableSet G)
     (hT : HasBoundedStrongType (linearizedNontangentialOperator Q θ K · · |>.toReal)
diff --git a/Carleson/MetricCarleson.lean b/Carleson/MetricCarleson.lean
@@ -24,7 +24,7 @@ variable {K : X → X → ℂ}
 /- Theorem 1.0.2 -/
 theorem metric_carleson [CompatibleFunctions ℝ X (defaultA a)]
   [IsCancellative X (defaultτ a)] [IsOneSidedKernel a K]
-    (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
+    (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
     (hF : MeasurableSet F) (hG : MeasurableSet G)
     (hT : HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a))
     (f : X → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
diff --git a/Carleson/ToMathlib/Analysis/Convolution.lean b/Carleson/ToMathlib/Analysis/Convolution.lean
@@ -41,12 +41,13 @@ protected theorem AEStronglyMeasurable.convolution [NormedSpace ℝ F] [AddGroup
 `enorm_convolution_le_eLpNorm_mul_eLpNorm`. -/
 lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm [AddGroup G]
     [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsNegInvariant]
-    [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
+    [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.HolderConjugate q)
     (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖)
     (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) :
     ∫⁻ a, ‖L (f a) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by
   rw [eLpNorm_comp_measurePreserving (p := q) hg (μ.measurePreserving_sub_left x₀) |>.symm]
-  replace hpq : 1 / 1 = 1 / p + 1 /q := by simpa using hpq.inv_add_inv_conj.symm
+  replace hpq : 1 / 1 = 1 / p + 1 /q := by
+    simpa using (ENNReal.HolderConjugate.inv_add_inv_eq_one p q).symm
   replace hpq : ENNReal.HolderTriple p q 1 := ⟨by simpa [eq_comm] using hpq⟩
   have hg' : AEStronglyMeasurable (g <| x₀ - ·) μ :=
     hg.comp_quasiMeasurePreserving <| quasiMeasurePreserving_sub_left μ x₀
@@ -58,7 +59,7 @@ lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm [AddGroup G]
 convolution of `f` and `g` exists everywhere. -/
 theorem ConvolutionExists.of_memLp_memLp [AddGroup G] [MeasurableAdd₂ G]
     [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant] [μ.IsAddLeftInvariant]
-    [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
+    [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.HolderConjugate q)
     (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ)
     (hg : AEStronglyMeasurable g μ) (hfp : MemLp f p μ) (hgq : MemLp g q μ) :
     ConvolutionExists f g L μ := by
@@ -70,7 +71,7 @@ theorem ConvolutionExists.of_memLp_memLp [AddGroup G] [MeasurableAdd₂ G]
 by `eLpNorm f p μ * eLpNorm g q μ`. -/
 theorem enorm_convolution_le_eLpNorm_mul_eLpNorm [NormedSpace ℝ F] [AddGroup G]
     [MeasurableAdd₂ G] [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant]
-    [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
+    [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.HolderConjugate q)
     (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖)
     (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) :
     ‖(f ⋆[L, μ] g) x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ :=
diff --git a/Carleson/ToMathlib/Data/Real/ConjExponents.lean b/Carleson/ToMathlib/Data/Real/ConjExponents.lean
@@ -2,24 +2,14 @@ import Mathlib.Data.Real.ConjExponents
 
 open scoped ENNReal
 
-namespace ENNReal
-namespace IsConjExponent
-
-variable {p q : ℝ≥0∞} (h : p.IsConjExponent q)
-
-section
+variable {p q : ℝ≥0∞} (h : p.HolderConjugate q)
 include h
 
-protected lemma toReal (hp : p ≠ ∞) (hq : q ≠ ∞) :
-    p.toReal.IsConjExponent q.toReal where
-  one_lt := by
-    rw [← ENNReal.ofReal_lt_iff_lt_toReal one_pos.le hp, ofReal_one]
-    exact h.one_le.lt_of_ne (fun p_eq_1 ↦ hq (by simpa [p_eq_1] using h.conj_eq))
-  inv_add_inv_conj := by
-    rw [← toReal_inv, ← toReal_inv, ← toReal_add, h.inv_add_inv_conj, ENNReal.toReal_eq_one_iff]
-    · exact ENNReal.inv_ne_top.mpr h.ne_zero
-    · exact ENNReal.inv_ne_top.mpr h.symm.ne_zero
-
-end
-end IsConjExponent
-end ENNReal
+protected lemma ENNReal.HolderConjugate.toReal_of_ne_top (hp : p ≠ ∞) (hq : q ≠ ∞) :
+    p.toReal.HolderConjugate q.toReal where
+  left_pos := toReal_pos (HolderConjugate.ne_zero p q) hp
+  right_pos := toReal_pos (HolderConjugate.ne_zero q p) hq
+  inv_add_inv' := by
+    rw [← toReal_inv, ← toReal_inv, ← toReal_add, h.inv_add_inv_eq_one, inv_one, toReal_one]
+    · exact ENNReal.inv_ne_top.mpr (HolderConjugate.ne_zero p q)
+    · exact ENNReal.inv_ne_top.mpr (HolderConjugate.ne_zero q p)
diff --git a/Carleson/ToMathlib/Data/Set/Lattice.lean b/Carleson/ToMathlib/Data/Set/Lattice.lean
diff --git a/Carleson/ToMathlib/MeasureTheory/Group/LIntegral.lean b/Carleson/ToMathlib/MeasureTheory/Group/LIntegral.lean
diff --git a/Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean b/Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean
@@ -5,7 +5,7 @@ import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
 import Mathlib.Analysis.Convolution
 import Carleson.ToMathlib.Data.Real.ConjExponents
 import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic
-import Carleson.ToMathlib.MeasureTheory.Group.LIntegral
+import Mathlib.MeasureTheory.Group.LIntegral
 import Carleson.ToMathlib.MeasureTheory.Integral.Periodic
 import Carleson.ToMathlib.MeasureTheory.Measure.Haar.Unique
 import Carleson.ToMathlib.MeasureTheory.Measure.Prod
@@ -59,7 +59,7 @@ theorem lintegral_prod_norm_pow_le' {α ι : Type*} [MeasurableSpace α] {μ : M
   · simp [eLpNorm, eLpNorm', p_ne_0 i hi, p_ne_top i hi]
 
 /-- **Hölder's inequality** for functions `α → ℝ≥0∞`, using exponents in `ℝ≥0∞`-/
-theorem lintegral_mul_le_eLpNorm_mul_eLqNorm {p q : ℝ≥0∞} (hpq : p.IsConjExponent q)
+theorem lintegral_mul_le_eLpNorm_mul_eLqNorm {p q : ℝ≥0∞} (hpq : p.HolderConjugate q)
     {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     ∫⁻ (a : α), (f * g) a ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by
   by_cases pq_top : p = ∞ ∨ q = ∞
@@ -69,8 +69,10 @@ theorem lintegral_mul_le_eLpNorm_mul_eLqNorm {p q : ℝ≥0∞} (hpq : p.IsConjE
     apply le_of_le_of_eq <| lintegral_mono_ae ((ae_le_essSup f).mono (fun a ha ↦ mul_right_mono ha))
     simp [eLpNorm, eLpNorm', eLpNormEssSup, hp, hpq.conj_eq, lintegral_const_mul'' _ hg]
   push_neg at pq_top
-  convert ENNReal.lintegral_mul_le_Lp_mul_Lq μ (hpq.toReal pq_top.1 pq_top.2) hf hg
-  all_goals simp [eLpNorm, eLpNorm', hpq.ne_zero, hpq.symm.ne_zero, pq_top]
+  have hp : p ≠ 0 := HolderConjugate.ne_zero p q
+  have hq : q ≠ 0 := HolderConjugate.ne_zero q p
+  convert ENNReal.lintegral_mul_le_Lp_mul_Lq μ (hpq.toReal_of_ne_top pq_top.1 pq_top.2) hf hg
+  all_goals simp [eLpNorm, eLpNorm', pq_top, hp, hq]
 
 end ENNReal
 
@@ -131,7 +133,7 @@ private theorem convolution_zero_of_c_nonpos [AddGroup G] {f : G → E} {g : G 
 
 -- Auxiliary inequality used to prove inequalities with simpler conditions on f and g.
 private theorem eLpNorm_top_convolution_le_aux [AddCommGroup G] {p q : ℝ≥0∞}
-    (hpq : p.IsConjExponent q) {f : G → E} {g : G → E'} (hf : AEMeasurable (‖f ·‖ₑ) μ)
+    (hpq : p.HolderConjugate q) {f : G → E} {g : G → E'} (hf : AEMeasurable (‖f ·‖ₑ) μ)
     (hg : ∀ x : G, AEMeasurable (‖g <| x - ·‖ₑ) μ)
     (hg' : ∀ x : G, eLpNorm (‖g <| x - ·‖ₑ) q μ = eLpNorm (‖g ·‖ₑ) q μ)
     (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
@@ -158,15 +160,15 @@ variable [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelS
 /-- Special case of **Young's convolution inequality** when `r = ∞`. -/
 theorem eLpNorm_top_convolution_le [MeasurableSpace E] [OpensMeasurableSpace E]
     [MeasurableSpace E'] [OpensMeasurableSpace E'] {p q : ℝ≥0∞}
-    (hpq : p.IsConjExponent q) {f : G → E} {g : G → E'} (hf : AEMeasurable f μ)
+    (hpq : p.HolderConjugate q) {f : G → E} {g : G → E'} (hf : AEMeasurable f μ)
     (hg : AEMeasurable g μ) (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
     eLpNorm (f ⋆[L, μ] g) ∞ μ ≤ ENNReal.ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
   refine eLpNorm_top_convolution_le_aux hpq hf.enorm ?_ ?_ c hL
   · intro x; exact (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x)).enorm
   · intro x; exact eLpNorm_comp_measurePreserving' hg (μ.measurePreserving_sub_left x)
 
 /-- Special case of **Young's convolution inequality** when `r = ∞`. -/
-theorem eLpNorm_top_convolution_le' {p q : ℝ≥0∞} (hpq : p.IsConjExponent q) {f : G → E} {g : G → E'}
+theorem eLpNorm_top_convolution_le' {p q : ℝ≥0∞} (hpq : p.HolderConjugate q) {f : G → E} {g : G → E'}
     (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (c : ℝ)
     (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
     eLpNorm (f ⋆[L, μ] g) ∞ μ ≤ ENNReal.ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
@@ -380,7 +382,7 @@ private theorem eLpNorm_convolution_le_of_norm_le_mul_aux {p q r : ℝ≥0∞}
   -- First use `eLpNorm_top_convolution_le` to handle the cases where any exponent is `∞`
   by_cases r_top : r = ∞
   · rw [r_top, ENNReal.inv_top, zero_add] at hpqr
-    have hpq : p.IsConjExponent q := by exact ⟨hpqr⟩
+    have hpq : p.HolderConjugate q := holderConjugate_iff.mpr hpqr
     rw [r_top]
     refine eLpNorm_top_convolution_le_aux hpq hf hg hg' c hL
   have hpq : 1 < p⁻¹ + q⁻¹ := by
diff --git a/Carleson/ToMathlib/Order/Chain.lean b/Carleson/ToMathlib/Order/Chain.lean
@@ -1,7 +1,8 @@
 import Mathlib.Order.Chain
-import Carleson.ToMathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Lattice
 
 lemma IsChain.pairwiseDisjoint_iUnion₂ {α β : Type*} [PartialOrder β] [OrderBot β]
     (c : Set (Set α)) (hc : IsChain (· ⊆ ·) c) (f : α → β)
-    (h : ∀ s ∈ c, s.PairwiseDisjoint f) : (⋃ s ∈ c, s).PairwiseDisjoint f :=
-  hc.directedOn.pairwise_iUnion₂ _ _ h
+    (h : ∀ s ∈ c, s.PairwiseDisjoint f) : (⋃ s ∈ c, s).PairwiseDisjoint f := by
+  apply Set.pairwise_iUnion₂ (directedOn hc)
+  exact fun s hs ↦ h s hs
diff --git a/Carleson/ToMathlib/RealInterpolation.lean b/Carleson/ToMathlib/RealInterpolation.lean
@@ -2100,7 +2100,7 @@ lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞
     ∫⁻ x : α, (f x) * g x ∂μ := by
   let A := spanningSets μ
   let g := trunc_cut f μ
-  have hpq' : p.IsConjExponent q := Real.IsConjExponent.mk hp hpq
+  have hpq' : p.HolderConjugate q := Real.holderConjugate_iff.mpr ⟨hp, hpq⟩
   have f_mul : ∀ n : ℕ, (g n) ^ p ≤ f * (g n) ^ (p - 1) := by
     intro n x
     simp only [g, Pi.pow_apply, Pi.mul_apply, trunc_cut, indicator]
@@ -2167,8 +2167,7 @@ lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞
         ext x
         rw [← ENNReal.rpow_mul]
         congr
-        refine Real.IsConjExponent.sub_one_mul_conj ?_
-        exact Real.IsConjExponent.mk hp hpq
+        refine Real.HolderConjugate.sub_one_mul_conj hpq'
       _ = (∫⁻ x : α, (g n x) ^ p ∂μ) ^ p⁻¹ := by
         rw [← ENNReal.rpow_neg]
         nth_rw 1 [← ENNReal.rpow_one (x := (∫⁻ x : α, (g n x) ^ (p) ∂μ))]
@@ -2222,7 +2221,7 @@ lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞
             ext z
             rw [← ENNReal.rpow_mul]
             congr
-            exact Real.IsConjExponent.sub_one_mul_conj hpq'
+            exact Real.HolderConjugate.sub_one_mul_conj hpq'
           _ < ⊤ := g_fin n
         · linarith
   apply eq_of_le_of_le
@@ -2287,8 +2286,8 @@ lemma lintegral_lintegral_pow_swap {α : Type u_1} {β : Type u_3} {p : ℝ} (hp
     ∫⁻ (y : β), (∫⁻ (x : α), (f x y) ^ p ∂μ) ^ p⁻¹ ∂ν := by
   rcases Decidable.lt_or_eq_of_le hp with one_lt_p | one_eq_p
   · let q := Real.conjExponent p
-    have hpq' : p.IsConjExponent q := Real.IsConjExponent.conjExponent one_lt_p
-    have one_lt_q : 1 < q := (Real.IsConjExponent.symm hpq').one_lt
+    have hpq' : p.HolderConjugate q := Real.HolderConjugate.conjExponent one_lt_p
+    have one_lt_q : 1 < q := (Real.HolderConjugate.symm hpq').lt
     have ineq : ∀ g ∈ {g' : α → ℝ≥0∞ | AEMeasurable g' μ ∧ ∫⁻ (z : α), (g' z) ^ q ∂μ ≤ 1},
         ∫⁻ x : α, (∫⁻ y : β, f x y ∂ν) * g x ∂μ ≤
         ∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ p⁻¹ ∂ν := by
@@ -2311,7 +2310,7 @@ lemma lintegral_lintegral_pow_swap {α : Type u_1} {β : Type u_3} {p : ℝ} (hp
         _ = (∫⁻ (x : α), f x y ^ p ∂μ) ^ p⁻¹ := by
           simp [one_div]
     nth_rw 1 [← one_div]
-    rw [representationLp (hp := one_lt_p) (hq := one_lt_q.le) (hpq := hpq'.inv_add_inv_conj)]
+    rw [representationLp (hp := one_lt_p) (hq := one_lt_q.le) (hpq := hpq'.inv_add_inv_eq_one)]
     · exact (iSup_le fun g ↦ iSup_le fun hg ↦ ineq g hg)
     · exact (aemeasurability_integral_component hf)
   · rw [← one_eq_p]
diff --git a/Carleson/TwoSidedCarleson/MainTheorem.lean b/Carleson/TwoSidedCarleson/MainTheorem.lean
@@ -24,7 +24,7 @@ variable [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a
 /-! ## Theorem 10.0.1 -/
 
 /- Theorem 10.0.1 -/
-theorem two_sided_metric_carleson (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
+theorem two_sided_metric_carleson (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
     (hF : MeasurableSet F) (hG : MeasurableSet G)
     (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a))
     {f : X → ℂ} (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cc40bfec1047f8c40fb3856921406f69431a735e",
+   "rev": "aa936c36e8484abd300577139faf8e945850831a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "471ff276892c3451a1d693477107e9c3a0c8ab85",
+   "rev": "ecaaeb0b44a8d5784f17bd417e83f44c906804ab",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
+   "rev": "0e05c2f090b7dd7a2f530bdc48a26b546f4837c7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5a7f12e78c70159bbf4e7d538f9cb67abe562996",
+   "rev": "613510345e4d4b3ce3d8c129595e7241990d5b39",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.18.0-rc1
+leanprover/lean4:v4.18.0
