chore: last upstreaming comment; minor golfs

Author: grunweg

Carleson/ToMathlib/Analysis/MeanInequalitiesPow.lean

@@ -1,6 +1,8 @@
 import Mathlib.Analysis.MeanInequalitiesPow
 import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
 
+-- Upstreaming status: looks useful and ready to go
+
 namespace ENNReal
 
 theorem rpow_add_le_mul_rpow_add_rpow' (z₁ z₂ : ℝ≥0∞) {p : ℝ} (hp : 0 ≤ p) :

Carleson/ToMathlib/HardyLittlewood.lean

@@ -870,21 +870,17 @@ theorem hasWeakType_maximalFunction_equal_exponents
     simp only [enorm_eq_self, mem_setOf_eq]
     exact fun ht ↦ ht.trans_le (f_mon hmn x)
   apply (rpow_le_rpow_iff p_pos).mp
-  rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity)]
-  rw [rpow_inv_rpow p_pos.ne']
-  by_cases ht : t = 0; · rw [ht]; simp [(zero_rpow_of_pos p_pos)]
-  have htp : (t : ℝ≥0∞) ^ (p : ℝ) ≠ 0 :=
-    (rpow_pos (coe_pos.mpr ((zero_le t).lt_of_ne' ht)) coe_ne_top).ne'
-  have htp' : (t : ℝ≥0∞) ^ (p : ℝ) ≠ ⊤ :=
-    ne_of_lt ((rpow_lt_top_iff_of_pos p_pos).mpr coe_lt_top)
-  refine (mul_le_iff_le_inv htp htp').mpr ?_
+  rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity), rpow_inv_rpow p_pos.ne']
+  by_cases ht : t = 0
+  · rw [ht]; simp [(zero_rpow_of_pos p_pos)]
+  refine (mul_le_iff_le_inv (by positivity) (by finiteness)).mpr ?_
   calc
   _ ≤ _ := measure_mono (hunion t)
   _ ≤ _ := by
     have := MeasureTheory.tendsto_measure_iUnion_atTop (μ := μ) hm
     refine le_of_tendsto_of_frequently this (.of_forall fun x ↦ ?_)
     dsimp only [Function.comp_apply]
-    refine (mul_le_iff_le_inv htp htp').mp ?_
+    refine (mul_le_iff_le_inv (by positivity) (by finiteness)).mp ?_
     rw [← rpow_inv_rpow (x := μ _) p_pos.ne', ← ENNReal.mul_rpow_of_nonneg _ _ (by positivity)]
     exact (rpow_le_rpow_iff p_pos).mpr (hestfin x t)
 

Carleson/ToMathlib/LorentzType.lean

@@ -397,12 +397,11 @@ lemma HasRestrictedWeakType'.hasLorentzType [SigmaFinite ν]
       rw [G_finite]
       unfold r
       apply (ENNReal.rpow_lt_top_iff_of_pos p_toReal_pos).mpr
-      apply ENNReal.div_lt_top _ (by simpa)
-      apply ENNReal.mul_ne_top hc hf.2.ne
+      have := hf.2.ne
+      exact ENNReal.div_lt_top (by finiteness) (by simpa)
     rcases ν.exists_subset_measure_lt_top hG' this with ⟨H, hH, H_subset_G', H_gt, H_finite⟩
     have H_pos := (zero_le _).trans_lt H_gt
-    have := (hT f hf H hH).2
-    apply this.not_gt
+    apply (hT f hf H hH).2.not_gt
     calc _
       _ < l * ν H := by
         rw [← ENNReal.lt_div_iff_mul_lt

Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean

@@ -783,8 +783,7 @@ lemma ζ_pos_iff_aux₀ (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q
 
 lemma inv_toReal_iff (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) :
     p₀⁻¹.toReal < p₁⁻¹.toReal ↔ p₁ < p₀ :=
-  Iff.trans (toReal_lt_toReal (ne_of_lt (inv_lt_top.mpr hp₀))
-    (ne_of_lt (inv_lt_top.mpr hp₁))) ENNReal.inv_lt_inv
+  Iff.trans (toReal_lt_toReal (inv_lt_top.mpr hp₀).ne (inv_lt_top.mpr hp₁).ne) ENNReal.inv_lt_inv
 
 lemma ζ_pos_iff (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁)
     (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) :

Carleson/ToMathlib/RealInterpolation/Minkowski.lean

@@ -979,7 +979,7 @@ lemma weaktype_estimate_trunc_top {C₁ : ℝ≥0} (hC₁ : 0 < C₁) {p p₁ q
         simp only [this, mul_zero, zero_le]
     · have snorm_p_pos : eLpNorm f p μ ≠ 0 := by
         intro snorm_0
-        apply Ne.symm (ne_of_lt snorm_pos)
+        apply snorm_pos.ne'
         apply eLpNormEssSup_eq_zero_iff.mpr
         exact (eLpNorm_eq_zero_iff hf.1 hp.ne').mp snorm_0
       -- XXX: these lines are the same as in the lemma above

Carleson/ToMathlib/WeakType.lean

@@ -42,7 +42,7 @@ lemma distibution_top (f : α → ε) (μ : Measure α) : distribution f ∞ μ
 lemma distribution_mono_right (h : t ≤ s) : distribution f s μ ≤ distribution f t μ :=
   measure_mono fun _ a ↦ lt_of_le_of_lt h a
 
-lemma distribution_mono_right' : (Antitone (fun t ↦ distribution f t μ)) :=
+lemma distribution_mono_right' : Antitone (fun t ↦ distribution f t μ) :=
   fun _ _ h ↦ distribution_mono_right h
 
 @[measurability, fun_prop]
@@ -57,9 +57,8 @@ lemma distribution_measurable {g : α' → ℝ≥0∞} (hg : Measurable g) :
 lemma distribution_toReal_le {f : α → ℝ≥0∞} :
     distribution (ENNReal.toReal ∘ f) t μ ≤ distribution f t μ := by
   simp_rw [distribution]
-  apply measure_mono
-  simp_rw [comp_apply, enorm_eq_self, setOf_subset_setOf]
-  exact fun x hx ↦ hx.trans_le enorm_toReal_le
+  gcongr with x
+  simp [comp_apply, enorm_eq_self]
 
 lemma distribution_toReal_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x ≠ ∞) :
     distribution (ENNReal.toReal ∘ f) t μ = distribution f t μ := by
@@ -75,9 +74,7 @@ lemma distribution_add_le_of_enorm {A : ℝ≥0∞}
       ({x | t < ‖g₁ x‖ₑ} ∪ {x | s < ‖g₂ x‖ₑ})) = 0 := by
     apply measure_mono_null ?_ h
     intro x
-    simp only [mem_diff, mem_setOf_eq, mem_union, not_or, not_lt, mem_compl_iff, not_le, and_imp]
-    refine fun h₁ h₂ h₃ ↦ lt_of_le_of_lt ?_ h₁
-    gcongr
+    simpa using fun h₁ h₂ h₃ ↦ lt_of_le_of_lt (by gcongr) h₁
   calc
     μ {x | A * (t + s) < ‖f x‖ₑ}
       ≤ μ ({x | t < ‖g₁ x‖ₑ} ∪ {x | s < ‖g₂ x‖ₑ}) := measure_mono_ae' h₁
@@ -106,6 +103,7 @@ lemma tendsto_measure_iUnion_distribution (t₀ : ℝ≥0∞) :
     _ ≤ t₀ + (↑a)⁻¹ := by gcongr
     _ < _ := h₁
 
+-- TODO: better lemma name!
 lemma select_neighborhood_distribution (t₀ : ℝ≥0∞) (l : ℝ≥0∞)
     (hu : l < distribution f t₀ μ) :
     ∃ n : ℕ, l < distribution f (t₀ + (↑n)⁻¹) μ := by
@@ -152,8 +150,8 @@ lemma continuousWithinAt_distribution (t₀ : ℝ≥0∞) :
           exact ⟨zero_le 0, zero_le ε⟩
       -- Case: 0 < distribution f t₀ μ
       · obtain ⟨n, wn⟩ :=
-          select_neighborhood_distribution t₀ _ (ENNReal.sub_lt_self db_not_top.ne_top
-              (ne_of_lt db_not_zero).symm (ne_of_lt ε_gt_0).symm)
+          select_neighborhood_distribution t₀ _
+            (ENNReal.sub_lt_self db_not_top.ne_top db_not_zero.ne' ε_gt_0.ne')
         use Iio (t₀ + (↑n)⁻¹)
         constructor
         · exact Iio_mem_nhds (lt_add_right t₀nottop.ne_top (ENNReal.inv_ne_zero.mpr (by finiteness)))

Carleson/TwoSidedCarleson/Basic.lean

@@ -110,15 +110,12 @@ lemma czOperator_welldefined {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr :
       · exact mKxg.nullMeasurableSet_support
   obtain ⟨M, hM⟩ := bdd_Kxg
   apply integrableOn_of_integrableOn_inter_support measurableSet_ball.compl
-  apply Measure.integrableOn_of_bounded
-  · apply ne_top_of_le_ne_top
-    · exact ne_of_lt hg.measure_support_lt
-    · apply measure_mono
-      trans support Kxg
-      · exact inter_subset_right
-      · exact support_mul_subset_right (K x) g
-  · exact mKxg
-  · exact hM
+  apply Measure.integrableOn_of_bounded ?_ mKxg hM
+  apply ne_top_of_le_ne_top (hg.measure_support_lt.ne)
+  apply measure_mono
+  trans support Kxg
+  · exact inter_subset_right
+  · exact support_mul_subset_right (K x) g
 
 -- 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) :