bump to nightly-2023-05-23-20

mathlib commit leanprover-community/mathlib@75e7fca

Mathbin/Analysis/Calculus/FderivMeasurable.lean

@@ -485,10 +485,10 @@ theorem aEMeasurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜] [M
   (measurable_deriv f).AEMeasurable
 #align ae_measurable_deriv aEMeasurable_deriv
 
-theorem aeStronglyMeasurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
-    [SecondCountableTopology F] (f : 𝕜 → F) (μ : Measure 𝕜) : AeStronglyMeasurable (deriv f) μ :=
-  (stronglyMeasurable_deriv f).AeStronglyMeasurable
-#align ae_strongly_measurable_deriv aeStronglyMeasurable_deriv
+theorem aEStronglyMeasurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
+    [SecondCountableTopology F] (f : 𝕜 → F) (μ : Measure 𝕜) : AEStronglyMeasurable (deriv f) μ :=
+  (stronglyMeasurable_deriv f).AEStronglyMeasurable
+#align ae_strongly_measurable_deriv aEStronglyMeasurable_deriv
 
 end fderiv
 
@@ -871,10 +871,10 @@ theorem aEMeasurable_derivWithin_Ici [MeasurableSpace F] [BorelSpace F] (μ : Me
   (measurable_derivWithin_Ici f).AEMeasurable
 #align ae_measurable_deriv_within_Ici aEMeasurable_derivWithin_Ici
 
-theorem aeStronglyMeasurable_derivWithin_Ici [SecondCountableTopology F] (μ : Measure ℝ) :
-    AeStronglyMeasurable (fun x => derivWithin f (Ici x) x) μ :=
-  (stronglyMeasurable_derivWithin_Ici f).AeStronglyMeasurable
-#align ae_strongly_measurable_deriv_within_Ici aeStronglyMeasurable_derivWithin_Ici
+theorem aEStronglyMeasurable_derivWithin_Ici [SecondCountableTopology F] (μ : Measure ℝ) :
+    AEStronglyMeasurable (fun x => derivWithin f (Ici x) x) μ :=
+  (stronglyMeasurable_derivWithin_Ici f).AEStronglyMeasurable
+#align ae_strongly_measurable_deriv_within_Ici aEStronglyMeasurable_derivWithin_Ici
 
 /-- The set of right differentiability points of a function taking values in a complete space is
 Borel-measurable. -/
@@ -901,10 +901,10 @@ theorem aEMeasurable_derivWithin_Ioi [MeasurableSpace F] [BorelSpace F] (μ : Me
   (measurable_derivWithin_Ioi f).AEMeasurable
 #align ae_measurable_deriv_within_Ioi aEMeasurable_derivWithin_Ioi
 
-theorem aeStronglyMeasurable_derivWithin_Ioi [SecondCountableTopology F] (μ : Measure ℝ) :
-    AeStronglyMeasurable (fun x => derivWithin f (Ioi x) x) μ :=
-  (stronglyMeasurable_derivWithin_Ioi f).AeStronglyMeasurable
-#align ae_strongly_measurable_deriv_within_Ioi aeStronglyMeasurable_derivWithin_Ioi
+theorem aEStronglyMeasurable_derivWithin_Ioi [SecondCountableTopology F] (μ : Measure ℝ) :
+    AEStronglyMeasurable (fun x => derivWithin f (Ioi x) x) μ :=
+  (stronglyMeasurable_derivWithin_Ioi f).AEStronglyMeasurable
+#align ae_strongly_measurable_deriv_within_Ioi aEStronglyMeasurable_derivWithin_Ioi
 
 end RightDeriv
 

Mathbin/Analysis/Calculus/ParametricIntegral.lean

@@ -74,8 +74,8 @@ ae-measurable for `x` in the same ball. See `has_fderiv_at_integral_of_dominated
 slightly less general but usually more useful version. -/
 theorem hasFDerivAt_integral_of_dominated_loc_of_lip' {F : H → α → E} {F' : α → H →L[𝕜] E} {x₀ : H}
     {bound : α → ℝ} {ε : ℝ} (ε_pos : 0 < ε)
-    (hF_meas : ∀ x ∈ ball x₀ ε, AeStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
-    (hF'_meas : AeStronglyMeasurable F' μ)
+    (hF_meas : ∀ x ∈ ball x₀ ε, AEStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
+    (hF'_meas : AEStronglyMeasurable F' μ)
     (h_lipsch : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖)
     (bound_integrable : Integrable (bound : α → ℝ) μ)
     (h_diff : ∀ᵐ a ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) :
@@ -169,8 +169,8 @@ theorem hasFDerivAt_integral_of_dominated_loc_of_lip' {F : H → α → E} {F' :
 (with a ball radius independent of `a`) with integrable Lipschitz bound, and `F x` is ae-measurable
 for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasFDerivAt_integral_of_dominated_loc_of_lip {F : H → α → E} {F' : α → H →L[𝕜] E} {x₀ : H}
-    {bound : α → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) μ)
-    (hF_int : Integrable (F x₀) μ) (hF'_meas : AeStronglyMeasurable F' μ)
+    {bound : α → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ)
+    (hF_int : Integrable (F x₀) μ) (hF'_meas : AEStronglyMeasurable F' μ)
     (h_lip : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs <| bound a) (fun x => F x a) (ball x₀ ε))
     (bound_integrable : Integrable (bound : α → ℝ) μ)
     (h_diff : ∀ᵐ a ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) :
@@ -191,8 +191,8 @@ derivative norm uniformly bounded by an integrable function (the ball radius is
 and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasFDerivAt_integral_of_dominated_of_fderiv_le {F : H → α → E} {F' : H → α → H →L[𝕜] E}
     {x₀ : H} {bound : α → ℝ} {ε : ℝ} (ε_pos : 0 < ε)
-    (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
-    (hF'_meas : AeStronglyMeasurable (F' x₀) μ)
+    (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
+    (hF'_meas : AEStronglyMeasurable (F' x₀) μ)
     (h_bound : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a)
     (bound_integrable : Integrable (bound : α → ℝ) μ)
     (h_diff : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x a) (F' x a) x) :
@@ -221,8 +221,8 @@ assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball ar
 (with ball radius independent of `a`) with integrable Lipschitz bound, and `F x` is
 ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasDerivAt_integral_of_dominated_loc_of_lip {F : 𝕜 → α → E} {F' : α → E} {x₀ : 𝕜} {ε : ℝ}
-    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) μ)
-    (hF_int : Integrable (F x₀) μ) (hF'_meas : AeStronglyMeasurable F' μ) {bound : α → ℝ}
+    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ)
+    (hF_int : Integrable (F x₀) μ) (hF'_meas : AEStronglyMeasurable F' μ) {bound : α → ℝ}
     (h_lipsch : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs <| bound a) (fun x => F x a) (ball x₀ ε))
     (bound_integrable : Integrable (bound : α → ℝ) μ)
     (h_diff : ∀ᵐ a ∂μ, HasDerivAt (fun x => F x a) (F' a) x₀) :
@@ -253,8 +253,8 @@ theorem hasDerivAt_integral_of_dominated_loc_of_lip {F : 𝕜 → α → E} {F'
 (with interval radius independent of `a`) with derivative uniformly bounded by an integrable
 function, and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le {F : 𝕜 → α → E} {F' : 𝕜 → α → E} {x₀ : 𝕜}
-    {ε : ℝ} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) μ)
-    (hF_int : Integrable (F x₀) μ) (hF'_meas : AeStronglyMeasurable (F' x₀) μ) {bound : α → ℝ}
+    {ε : ℝ} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ)
+    (hF_int : Integrable (F x₀) μ) (hF'_meas : AEStronglyMeasurable (F' x₀) μ) {bound : α → ℝ}
     (h_bound : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
     (h_diff : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x) :
     Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ a, F n a ∂μ) (∫ a, F' x₀ a ∂μ) x₀ :=

Mathbin/Analysis/Calculus/ParametricIntervalIntegral.lean

@@ -33,9 +33,9 @@ namespace intervalIntegral
 (with a ball radius independent of `a`) with integrable Lipschitz bound, and `F x` is ae-measurable
 for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasFDerivAt_integral_of_dominated_loc_of_lip {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H}
-    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) (μ.restrict (Ι a b)))
+    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
     (hF_int : IntervalIntegrable (F x₀) μ a b)
-    (hF'_meas : AeStronglyMeasurable F' (μ.restrict (Ι a b)))
+    (hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b)))
     (h_lip :
       ∀ᵐ t ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs <| bound t) (fun x => F x t) (ball x₀ ε))
     (bound_integrable : IntervalIntegrable bound μ a b)
@@ -57,9 +57,9 @@ derivative norm uniformly bounded by an integrable function (the ball radius is
 and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasFDerivAt_integral_of_dominated_of_fderiv_le {F : H → ℝ → E} {F' : H → ℝ → H →L[𝕜] E}
     {x₀ : H} (ε_pos : 0 < ε)
-    (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) (μ.restrict (Ι a b)))
+    (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
     (hF_int : IntervalIntegrable (F x₀) μ a b)
-    (hF'_meas : AeStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)))
+    (hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)))
     (h_bound : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t)
     (bound_integrable : IntervalIntegrable bound μ a b)
     (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x t) (F' x t) x) :
@@ -78,9 +78,9 @@ assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball ar
 (with ball radius independent of `a`) with integrable Lipschitz bound, and `F x` is
 ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasDerivAt_integral_of_dominated_loc_of_lip {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜}
-    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) (μ.restrict (Ι a b)))
+    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
     (hF_int : IntervalIntegrable (F x₀) μ a b)
-    (hF'_meas : AeStronglyMeasurable F' (μ.restrict (Ι a b)))
+    (hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b)))
     (h_lipsch :
       ∀ᵐ t ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs <| bound t) (fun x => F x t) (ball x₀ ε))
     (bound_integrable : IntervalIntegrable (bound : ℝ → ℝ) μ a b)
@@ -101,9 +101,9 @@ assuming `F x₀` is integrable, `x ↦ F x a` is differentiable on an interval
 (with interval radius independent of `a`) with derivative uniformly bounded by an integrable
 function, and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le {F : 𝕜 → ℝ → E} {F' : 𝕜 → ℝ → E} {x₀ : 𝕜}
-    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AeStronglyMeasurable (F x) (μ.restrict (Ι a b)))
+    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
     (hF_int : IntervalIntegrable (F x₀) μ a b)
-    (hF'_meas : AeStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)))
+    (hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)))
     (h_bound : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t)
     (bound_integrable : IntervalIntegrable bound μ a b)
     (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x t) (F' x t) x) :