bump to nightly-2023-05-21-14

mathlib commit leanprover-community/mathlib@33c67ae

Mathbin/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

@@ -327,9 +327,9 @@ basic open set `D(f.denom)`-/
 def sectionInBasicOpen (x : ProjectiveSpectrum.top 𝒜) :
     ∀ f : at x, (Proj.structureSheaf 𝒜).1.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f.den)) :=
   fun f =>
-  ⟨fun y => Quotient.mk'' ⟨f.deg, ⟨f.num, f.num_mem_deg⟩, ⟨f.den, f.denom_mem_deg⟩, y.2⟩, fun y =>
+  ⟨fun y => Quotient.mk'' ⟨f.deg, ⟨f.num, f.num_mem_deg⟩, ⟨f.den, f.den_mem_deg⟩, y.2⟩, fun y =>
     ⟨ProjectiveSpectrum.basicOpen 𝒜 f.den, y.2,
-      ⟨𝟙 _, ⟨f.deg, ⟨⟨f.num, f.num_mem_deg⟩, ⟨f.den, f.denom_mem_deg⟩, fun z => ⟨z.2, rfl⟩⟩⟩⟩⟩⟩
+      ⟨𝟙 _, ⟨f.deg, ⟨⟨f.num, f.num_mem_deg⟩, ⟨f.den, f.den_mem_deg⟩, fun z => ⟨z.2, rfl⟩⟩⟩⟩⟩⟩
 #align algebraic_geometry.section_in_basic_open AlgebraicGeometry.sectionInBasicOpen
 
 /-- Given any point `x` and `f` in the homogeneous localization at `x`, there is an element in the

Mathbin/MeasureTheory/Category/Meas.lean

@@ -130,7 +130,7 @@ warning: Borel -> borel is a dubious translation:
 lean 3 declaration is
   CategoryTheory.Functor.{u1, u1, succ u1, succ u1} TopCat.{u1} TopCat.largeCategory.{u1} Meas.{u1} Meas.largeCategory.{u1}
 but is expected to have type
-  forall (α : Type.{u1}) [_inst_1 : TopologicalSpace.{u1} α], MeasurableSpace.{u1} α
+  forall (α : Type.{u1}) [inst._@.Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._hyg.44 : TopologicalSpace.{u1} α], MeasurableSpace.{u1} α
 Case conversion may be inaccurate. Consider using '#align Borel borelₓ'. -/
 /-- The Borel functor, the canonical embedding of topological spaces into measurable spaces. -/
 @[reducible]

Mathbin/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

@@ -53,7 +53,7 @@ theorem measurable_of_tendsto_eNNReal {f : ℕ → α → ℝ≥0∞} {g : α 
 theorem measurable_of_tendsto_nnreal' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : Filter ι) [NeBot u]
     [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) :
     Measurable g := by
-  simp_rw [← measurable_coe_nNReal_eNNReal_iff] at hf⊢
+  simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf⊢
   refine' measurable_of_tendsto_ennreal' u hf _
   rw [tendsto_pi_nhds] at lim⊢
   exact fun x => (ennreal.continuous_coe.tendsto (g x)).comp (limUnder x)

Mathbin/MeasureTheory/Constructions/Polish.lean

@@ -661,7 +661,7 @@ theorem MeasurableSet.image_of_measurable_injOn [SecondCountableTopology β] (hs
     f_meas.exists_continuous
   have M : measurable_set[@borel γ t'] s :=
     @Continuous.measurable γ γ t' (@borel γ t')
-      (@BorelSpace.opens_measurable γ t' (@borel γ t')
+      (@BorelSpace.opensMeasurable γ t' (@borel γ t')
         (by
           constructor
           rfl))
@@ -730,7 +730,7 @@ theorem isClopenable_iff_measurableSet : IsClopenable s ↔ MeasurableSet s :=
   -- the set `s` is measurable for `t'` as it is closed.
   have M : @MeasurableSet γ (@borel γ t') s :=
     @IsClosed.measurableSet γ s t' (@borel γ t')
-      (@BorelSpace.opens_measurable γ t' (@borel γ t')
+      (@BorelSpace.opensMeasurable γ t' (@borel γ t')
         (by
           constructor
           rfl))

Mathbin/MeasureTheory/Constructions/Prod/Basic.lean

@@ -184,7 +184,7 @@ theorem measurable_measure_prod_mk_left_finite [FiniteMeasure ν] {s : Set (α 
       measure_Union (fun i j hij => Disjoint.preimage _ (h1f hij)) fun i =>
         measurable_prod_mk_left (h2f i)
     simp_rw [this]
-    apply Measurable.eNNReal_tsum h3f
+    apply Measurable.ennreal_tsum h3f
 #align measurable_measure_prod_mk_left_finite measurable_measure_prod_mk_left_finite
 
 /-- If `ν` is a σ-finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is

Mathbin/MeasureTheory/Constructions/Prod/Integral.lean

@@ -102,7 +102,7 @@ theorem MeasureTheory.StronglyMeasurable.integral_prod_right [SigmaFinite ν] 
       exact ⟨(x, z), rfl⟩
     simp only [simple_func.integral_eq_sum_of_subset (this _)]
     refine' Finset.stronglyMeasurable_sum _ fun x _ => _
-    refine' (Measurable.eNNReal_toReal _).StronglyMeasurable.smul_const _
+    refine' (Measurable.ennreal_toReal _).StronglyMeasurable.smul_const _
     simp (config := { singlePass := true }) only [simple_func.coe_comp, preimage_comp]
     apply measurable_measure_prod_mk_left
     exact (s n).measurableSet_fiber x
@@ -169,7 +169,7 @@ variable [SigmaFinite ν]
 theorem integrable_measure_prod_mk_left {s : Set (α × β)} (hs : MeasurableSet s)
     (h2s : (μ.Prod ν) s ≠ ∞) : Integrable (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ :=
   by
-  refine' ⟨(measurable_measure_prod_mk_left hs).eNNReal_toReal.AEMeasurable.AeStronglyMeasurable, _⟩
+  refine' ⟨(measurable_measure_prod_mk_left hs).ennreal_toReal.AEMeasurable.AeStronglyMeasurable, _⟩
   simp_rw [has_finite_integral, ennnorm_eq_of_real to_real_nonneg]
   convert h2s.lt_top using 1; simp_rw [prod_apply hs]; apply lintegral_congr_ae
   refine' (ae_measure_lt_top hs h2s).mp _; apply eventually_of_forall; intro x hx

Mathbin/MeasureTheory/Decomposition/Lebesgue.lean

@@ -751,7 +751,7 @@ instance (priority := 100) haveLebesgueDecomposition_of_sigmaFinite (μ ν : Mea
     refine' ⟨⟨ξ, f⟩, _, _, _⟩
     ·
       exact
-        Measurable.eNNReal_tsum' fun n =>
+        Measurable.ennreal_tsum' fun n =>
           Measurable.indicator (measurable_rn_deriv (μn n) (νn n)) (S.set_mem n)
     -- We show that `ξ` is mutually singular with respect to `ν`
     · choose A hA₁ hA₂ hA₃ using fun n => mutually_singular_singular_part (μn n) (νn n)

Mathbin/MeasureTheory/Function/ConditionalExpectation/Basic.lean

@@ -1122,7 +1122,7 @@ theorem condexpL2_ae_eq_zero_of_ae_eq_zero (hs : measurable_set[m] s) (hμs : μ
     dsimp only at hx
     rw [Pi.zero_apply] at hx⊢
     · rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
-    · refine' Measurable.coe_nNReal_eNNReal (Measurable.nnnorm _)
+    · refine' Measurable.coe_nnreal_ennreal (Measurable.nnnorm _)
       rw [Lp_meas_coe]
       exact (Lp.strongly_measurable _).Measurable
   refine' le_antisymm _ (zero_le _)

Mathbin/MeasureTheory/Function/ConditionalExpectation/Real.lean

@@ -206,8 +206,8 @@ theorem ae_bdd_condexp_of_ae_bdd {R : ℝ≥0} {f : α → ℝ} (hbdd : ∀ᵐ x
         lt_of_le_of_lt _
           (integrable_condexp.integrable_on : integrable_on (μ[f|m]) { x | ↑R < |(μ[f|m]) x| } μ).2⟩
     refine'
-      set_lintegral_mono (Measurable.nnnorm _).coe_nNReal_eNNReal
-        (strongly_measurable_condexp.mono hnm).Measurable.nnnorm.coe_nNReal_eNNReal fun x hx => _
+      set_lintegral_mono (Measurable.nnnorm _).coe_nnreal_ennreal
+        (strongly_measurable_condexp.mono hnm).Measurable.nnnorm.coe_nnreal_ennreal fun x hx => _
     · exact measurable_const
     · rw [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg R.coe_nonneg]
       exact Subtype.mk_le_mk.2 (le_of_lt hx)

Mathbin/MeasureTheory/Function/L1Space.lean

@@ -1030,7 +1030,7 @@ theorem mem_ℒ1_toReal_of_lintegral_ne_top {f : α → ℝ≥0∞} (hfm : AEMea
   by
   rw [mem_ℒp, snorm_one_eq_lintegral_nnnorm]
   exact
-    ⟨(AEMeasurable.eNNReal_toReal hfm).AeStronglyMeasurable,
+    ⟨(AEMeasurable.ennreal_toReal hfm).AeStronglyMeasurable,
       has_finite_integral_to_real_of_lintegral_ne_top hfi⟩
 #align measure_theory.mem_ℒ1_to_real_of_lintegral_ne_top MeasureTheory.mem_ℒ1_toReal_of_lintegral_ne_top
 

Mathbin/MeasureTheory/Function/LocallyIntegrable.lean

@@ -340,7 +340,7 @@ theorem MonotoneOn.integrableOn_of_measure_ne_top (hmono : MonotoneOn f s) {a b
   have A : integrable_on (fun x => C) s μ := by
     simp only [hs.lt_top, integrable_on_const, or_true_iff]
   refine'
-    integrable.mono' A (aEMeasurable_restrict_of_monotoneOn h's hmono).AeStronglyMeasurable
+    integrable.mono' A (aemeasurable_restrict_of_monotoneOn h's hmono).AeStronglyMeasurable
       ((ae_restrict_iff' h's).mpr <| ae_of_all _ fun y hy => hC (f y) (mem_image_of_mem f hy))
 #align monotone_on.integrable_on_of_measure_ne_top MonotoneOn.integrableOn_of_measure_ne_top
 

Mathbin/MeasureTheory/Function/LpSpace.lean

@@ -1008,7 +1008,7 @@ theorem snorm'_trim (hm : m ≤ m0) {f : α → E} (hf : strongly_measurable[m]
   simp_rw [snorm']
   congr 1
   refine' lintegral_trim hm _
-  refine' @Measurable.pow_const _ _ _ _ _ _ _ m _ (@Measurable.coe_nNReal_eNNReal _ m _ _) _
+  refine' @Measurable.pow_const _ _ _ _ _ _ _ m _ (@Measurable.coe_nnreal_ennreal _ m _ _) _
   apply @strongly_measurable.measurable
   exact @strongly_measurable.nnnorm α m _ _ _ hf
 #align measure_theory.snorm'_trim MeasureTheory.snorm'_trim
@@ -1599,9 +1599,9 @@ theorem ae_bdd_liminf_atTop_rpow_of_snorm_bdd {p : ℝ≥0∞} {f : ℕ → α 
   have hp : p ≠ 0 := fun h => by simpa [h] using hp0
   have hp' : p ≠ ∞ := fun h => by simpa [h] using hp0
   refine'
-    ae_lt_top (measurable_liminf fun n => (hfmeas n).nnnorm.coe_nNReal_eNNReal.pow_const p.to_real)
+    ae_lt_top (measurable_liminf fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.to_real)
       (lt_of_le_of_lt
-          (lintegral_liminf_le fun n => (hfmeas n).nnnorm.coe_nNReal_eNNReal.pow_const p.to_real)
+          (lintegral_liminf_le fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.to_real)
           (lt_of_le_of_lt _
             (ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top :
               ↑R ^ p.to_real < ∞))).Ne
@@ -2964,7 +2964,7 @@ private theorem tsum_nnnorm_sub_ae_lt_top {f : ℕ → α → E} (hf : ∀ n, Ae
   have rpow_ae_lt_top : ∀ᵐ x ∂μ, (∑' i, ‖f (i + 1) x - f i x‖₊ : ℝ≥0∞) ^ p < ∞ :=
     by
     refine' ae_lt_top' (AEMeasurable.pow_const _ _) h_integral.ne
-    exact AEMeasurable.eNNReal_tsum fun n => ((hf (n + 1)).sub (hf n)).ennnorm
+    exact AEMeasurable.ennreal_tsum fun n => ((hf (n + 1)).sub (hf n)).ennnorm
   refine' rpow_ae_lt_top.mono fun x hx => _
   rwa [← ENNReal.lt_rpow_one_div_iff hp_pos,
     ENNReal.top_rpow_of_pos (by simp [hp_pos] : 0 < 1 / p)] at hx

Mathbin/MeasureTheory/Function/SpecialFunctions/Basic.lean

@@ -238,9 +238,9 @@ instance NNReal.hasMeasurablePow : MeasurablePow ℝ≥0 ℝ :=
 
 instance ENNReal.hasMeasurablePow : MeasurablePow ℝ≥0∞ ℝ :=
   by
-  refine' ⟨ENNReal.measurable_of_measurable_nNReal_prod _ _⟩
+  refine' ⟨ENNReal.measurable_of_measurable_nnreal_prod _ _⟩
   · simp_rw [ENNReal.coe_rpow_def]
-    refine' Measurable.ite _ measurable_const (measurable_fst.pow measurable_snd).coe_nNReal_eNNReal
+    refine' Measurable.ite _ measurable_const (measurable_fst.pow measurable_snd).coe_nnreal_ennreal
     exact
       MeasurableSet.inter (measurable_fst (measurable_set_singleton 0))
         (measurable_snd measurableSet_Iio)

Mathbin/MeasureTheory/Integral/Bochner.lean

@@ -1611,7 +1611,7 @@ theorem integral_tsum {ι} [Countable ι] {f : ι → α → E} (hf : ∀ i, AeS
   have hhh : ∀ᵐ a : α ∂μ, Summable fun n => (‖f n a‖₊ : ℝ) :=
     by
     rw [← lintegral_tsum hf''] at hf'
-    refine' (ae_lt_top' (AEMeasurable.eNNReal_tsum hf'') hf').mono _
+    refine' (ae_lt_top' (AEMeasurable.ennreal_tsum hf'') hf').mono _
     intro x hx
     rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]
     exact hx.ne
@@ -1623,8 +1623,8 @@ theorem integral_tsum {ι} [Countable ι] {f : ι → α → E} (hf : ∀ i, AeS
     rfl
   · simp_rw [← coe_nnnorm, ← NNReal.coe_tsum]
     rw [aeStronglyMeasurable_iff_aEMeasurable]
-    apply AEMeasurable.coe_nNReal_real
-    apply AEMeasurable.nNReal_tsum
+    apply AEMeasurable.coe_nnreal_real
+    apply AEMeasurable.nnreal_tsum
     exact fun i => (hf i).nnnorm.AEMeasurable
   · dsimp [has_finite_integral]
     have : (∫⁻ a, ∑' n, ‖f n a‖₊ ∂μ) < ⊤ := by rwa [lintegral_tsum hf'', lt_top_iff_ne_top]
@@ -1849,8 +1849,8 @@ theorem integral_mul_norm_le_Lp_mul_Lq {E} [NormedAddCommGroup E] {f g : α →
       · exact ENNReal.coe_ne_top
   ·
     exact
-      ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.1.nnnorm.AEMeasurable.coe_nNReal_eNNReal
-        hg.1.nnnorm.AEMeasurable.coe_nNReal_eNNReal
+      ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.1.nnnorm.AEMeasurable.coe_nnreal_ennreal
+        hg.1.nnnorm.AEMeasurable.coe_nnreal_ennreal
 #align measure_theory.integral_mul_norm_le_Lp_mul_Lq MeasureTheory.integral_mul_norm_le_Lp_mul_Lq
 
 /-- Hölder's inequality for functions `α → ℝ`. The integral of the product of two nonnegative

Mathbin/MeasureTheory/Integral/Layercake.lean

@@ -272,7 +272,7 @@ theorem lintegral_rpow_eq_lintegral_meas_le_mul (μ : Measure α) [SigmaFinite 
   rw [← key, ← lintegral_const_mul (ENNReal.ofReal p)] <;> simp_rw [obs]
   · congr with ω
     rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel' (f ω ^ p) p_pos.ne.symm]
-  · exact ((f_mble.pow measurable_const).div_const p).eNNReal_ofReal
+  · exact ((f_mble.pow measurable_const).div_const p).ennreal_ofReal
 #align measure_theory.lintegral_rpow_eq_lintegral_meas_le_mul MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul
 
 end MeasureTheory

Mathbin/MeasureTheory/Integral/Lebesgue.lean

@@ -1066,7 +1066,7 @@ theorem lintegral_liminf_le' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, AE
     (∫⁻ a, liminf (fun n => f n a) atTop ∂μ) = ∫⁻ a, ⨆ n : ℕ, ⨅ i ≥ n, f i a ∂μ := by
       simp only [liminf_eq_supr_infi_of_nat]
     _ = ⨆ n : ℕ, ∫⁻ a, ⨅ i ≥ n, f i a ∂μ :=
-      (lintegral_supr' (fun n => aEMeasurable_binfi _ (to_countable _) h_meas)
+      (lintegral_supr' (fun n => aemeasurable_biInf _ (to_countable _) h_meas)
         (ae_of_all μ fun a n m hnm => iInf_le_iInf_of_subset fun i hi => le_trans hnm hi))
     _ ≤ ⨆ n : ℕ, ⨅ i ≥ n, ∫⁻ a, f i a ∂μ := (iSup_mono fun n => le_infi₂_lintegral _)
     _ = atTop.liminf fun n => ∫⁻ a, f n a ∂μ := Filter.liminf_eq_iSup_iInf_of_nat.symm
@@ -1090,7 +1090,7 @@ theorem limsup_lintegral_le {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0
       by
       refine' (lintegral_infi _ _ _).symm
       · intro n
-        exact measurable_bsupr _ (to_countable _) hf_meas
+        exact measurable_biSup _ (to_countable _) hf_meas
       · intro n m hnm a
         exact iSup_le_iSup_of_subset fun i hi => le_trans hnm hi
       · refine' ne_top_of_le_ne_top h_fin (lintegral_mono_ae _)

Mathbin/MeasureTheory/Integral/SetIntegral.lean

@@ -625,7 +625,7 @@ theorem set_integral_gt_gt {R : ℝ} {f : α → ℝ} (hR : 0 ≤ R) (hfm : Meas
     by
     refine' ⟨ae_strongly_measurable_const, lt_of_le_of_lt _ hfint.2⟩
     refine'
-      set_lintegral_mono (Measurable.nnnorm _).coe_nNReal_eNNReal hfm.nnnorm.coe_nnreal_ennreal
+      set_lintegral_mono (Measurable.nnnorm _).coe_nnreal_ennreal hfm.nnnorm.coe_nnreal_ennreal
         fun x hx => _
     · exact measurable_const
     · simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR,

Mathbin/MeasureTheory/Integral/VitaliCaratheodory.lean

@@ -189,15 +189,15 @@ theorem exists_le_lowerSemicontinuous_lintegral_ge (f : α → ℝ≥0∞) (hf :
   ·
     calc
       (∫⁻ x, ∑' n : ℕ, g n x ∂μ) = ∑' n, ∫⁻ x, g n x ∂μ := by
-        rw [lintegral_tsum fun n => (gcont n).Measurable.coe_nNReal_eNNReal.AEMeasurable]
+        rw [lintegral_tsum fun n => (gcont n).Measurable.coe_nnreal_ennreal.AEMeasurable]
       _ ≤ ∑' n, (∫⁻ x, eapprox_diff f n x ∂μ) + δ n := (ENNReal.tsum_le_tsum hg)
       _ = (∑' n, ∫⁻ x, eapprox_diff f n x ∂μ) + ∑' n, δ n := ENNReal.tsum_add
       _ ≤ (∫⁻ x : α, f x ∂μ) + ε := by
         refine' add_le_add _ hδ.le
         rw [← lintegral_tsum]
         · simp_rw [tsum_eapprox_diff f hf, le_refl]
         · intro n
-          exact (simple_func.measurable _).coe_nNReal_eNNReal.AEMeasurable
+          exact (simple_func.measurable _).coe_nnreal_ennreal.AEMeasurable
 
 #align measure_theory.exists_le_lower_semicontinuous_lintegral_ge MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge
 
@@ -213,7 +213,7 @@ theorem exists_lt_lowerSemicontinuous_lintegral_ge [SigmaFinite μ] (f : α →
   have : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).ne'
   rcases exists_pos_lintegral_lt_of_sigma_finite μ this with ⟨w, wpos, wmeas, wint⟩
   let f' x := ((f x + w x : ℝ≥0) : ℝ≥0∞)
-  rcases exists_le_lower_semicontinuous_lintegral_ge μ f' (fmeas.add wmeas).coe_nNReal_eNNReal
+  rcases exists_le_lower_semicontinuous_lintegral_ge μ f' (fmeas.add wmeas).coe_nnreal_ennreal
       this with
     ⟨g, le_g, gcont, gint⟩
   refine' ⟨g, fun x => _, gcont, _⟩

Mathbin/MeasureTheory/Measure/FiniteMeasure.lean

@@ -317,7 +317,7 @@ def testAgainstNn (μ : FiniteMeasureCat Ω) (f : Ω →ᵇ ℝ≥0) : ℝ≥0 :
 theorem BoundedContinuousFunction.Nnreal.to_eNNReal_comp_measurable {Ω : Type _}
     [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (f : Ω →ᵇ ℝ≥0) :
     Measurable fun ω => (f ω : ℝ≥0∞) :=
-  measurable_coe_nNReal_eNNReal.comp f.Continuous.Measurable
+  measurable_coe_nnreal_ennreal.comp f.Continuous.Measurable
 #align bounded_continuous_function.nnreal.to_ennreal_comp_measurable BoundedContinuousFunction.Nnreal.to_eNNReal_comp_measurable
 
 theorem MeasureTheory.lintegral_lt_top_of_bounded_continuous_to_nNReal (μ : Measure Ω)