refactor(measure_theory/integral): restrict interval integrals to rea…

…l intervals (#12754)

This way `∫ x in 0 .. 1, (1 : real)` means what it should, not `∫ x : nat in 0 .. 1, (1 : real)`.

src/analysis/calculus/parametric_interval_integral.lean

@@ -16,21 +16,20 @@ integrals.  -/
 open topological_space measure_theory filter metric
 open_locale topological_space filter interval
 
-variables {α 𝕜 : Type*} [measurable_space α] [linear_order α] [topological_space α]
-          [order_topology α] [opens_measurable_space α] {μ : measure α} [is_R_or_C 𝕜]
+variables {𝕜 : Type*} [is_R_or_C 𝕜] {μ : measure ℝ}
           {E : Type*} [normed_group E] [normed_space ℝ E] [normed_space 𝕜 E]
           [complete_space E] [second_countable_topology E]
           [measurable_space E] [borel_space E]
           {H : Type*} [normed_group H] [normed_space 𝕜 H] [second_countable_topology $ H →L[𝕜] E]
-          {a b : α} {bound : α → ℝ} {ε : ℝ}
+          {a b ε : ℝ} {bound : ℝ → ℝ}
 
 namespace interval_integral
 
 /-- Differentiation under integral of `x ↦ ∫ t in a..b, F x t` at a given point `x₀`, assuming
 `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball around `x₀` for ae `a`
 (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₀`. -/
-lemma has_fderiv_at_integral_of_dominated_loc_of_lip {F : H → α → E} {F' : α → (H →L[𝕜] E)} {x₀ : H}
+lemma has_fderiv_at_integral_of_dominated_loc_of_lip {F : H → ℝ → E} {F' : ℝ → (H →L[𝕜] E)} {x₀ : H}
   (ε_pos : 0 < ε)
   (hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
   (hF_int : interval_integrable (F x₀) μ a b)
@@ -52,7 +51,7 @@ end
 `F x₀` is integrable, `x ↦ F x a` is differentiable on a ball around `x₀` for ae `a` with
 derivative norm uniformly bounded by an integrable function (the ball radius is independent of `a`),
 and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
-lemma has_fderiv_at_integral_of_dominated_of_fderiv_le {F : H → α → E} {F' : H → α → (H →L[𝕜] E)}
+lemma has_fderiv_at_integral_of_dominated_of_fderiv_le {F : H → ℝ → E} {F' : H → ℝ → (H →L[𝕜] E)}
   {x₀ : H} (ε_pos : 0 < ε)
   (hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
   (hF_int : interval_integrable (F x₀) μ a b)
@@ -72,14 +71,14 @@ end
 assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball around `x₀` for ae `a`
 (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₀`. -/
-lemma has_deriv_at_integral_of_dominated_loc_of_lip {F : 𝕜 → α → E} {F' : α → E} {x₀ : 𝕜}
+lemma has_deriv_at_integral_of_dominated_loc_of_lip {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜}
   (ε_pos : 0 < ε)
   (hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
   (hF_int : interval_integrable (F x₀) μ a b)
   (hF'_meas : ae_measurable F' (μ.restrict (Ι a b)))
   (h_lipsch : ∀ᵐ t ∂μ, t ∈ Ι a b →
     lipschitz_on_with (real.nnabs $ bound t) (λ x, F x t) (ball x₀ ε))
-  (bound_integrable : interval_integrable (bound : α → ℝ) μ a b)
+  (bound_integrable : interval_integrable (bound : ℝ → ℝ) μ a b)
   (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → has_deriv_at (λ x, F x t) (F' t) x₀) :
   (interval_integrable F' μ a b) ∧
     has_deriv_at (λ x, ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀ :=
@@ -95,7 +94,7 @@ end
 assuming `F x₀` is integrable, `x ↦ F x a` is differentiable on an interval around `x₀` for ae `a`
 (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₀`. -/
-lemma has_deriv_at_integral_of_dominated_loc_of_deriv_le {F : 𝕜 → α → E} {F' : 𝕜 → α → E} {x₀ : 𝕜}
+lemma has_deriv_at_integral_of_dominated_loc_of_deriv_le {F : 𝕜 → ℝ → E} {F' : 𝕜 → ℝ → E} {x₀ : 𝕜}
   (ε_pos : 0 < ε)
   (hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
   (hF_int : interval_integrable (F x₀) μ a b)

src/measure_theory/integral/integral_eq_improper.lean

@@ -397,36 +397,33 @@ end integral
 
 section integrable_of_interval_integral
 
-variables {α ι E : Type*}
-          [topological_space α] [linear_order α] [order_closed_topology α]
-          [measurable_space α] [opens_measurable_space α] {μ : measure α}
+variables {ι E : Type*} {μ : measure ℝ}
           {l : filter ι} [filter.ne_bot l] [is_countably_generated l]
           [measurable_space E] [normed_group E] [borel_space E]
-          {a b : ι → α} {f : α → E}
+          {a b : ι → ℝ} {f : ℝ → E}
 
-lemma integrable_of_interval_integral_norm_bounded [no_min_order α] [nonempty α]
+lemma integrable_of_interval_integral_norm_bounded
   (I : ℝ) (hfi : ∀ i, integrable_on f (Ioc (a i) (b i)) μ)
   (ha : tendsto a l at_bot) (hb : tendsto b l at_top)
   (h : ∀ᶠ i in l, ∫ x in a i .. b i, ∥f x∥ ∂μ ≤ I) :
   integrable f μ :=
 begin
-  let c : α := classical.choice ‹_›,
   have hφ : ae_cover μ l _ := ae_cover_Ioc ha hb,
   refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp _),
-  filter_upwards [ha.eventually (eventually_le_at_bot c), hb.eventually (eventually_ge_at_top c)]
+  filter_upwards [ha.eventually (eventually_le_at_bot 0), hb.eventually (eventually_ge_at_top 0)]
     with i hai hbi ht,
   rwa ←interval_integral.integral_of_le (hai.trans hbi)
 end
 
-lemma integrable_of_interval_integral_norm_tendsto [no_min_order α] [nonempty α]
+lemma integrable_of_interval_integral_norm_tendsto
   (I : ℝ) (hfi : ∀ i, integrable_on f (Ioc (a i) (b i)) μ)
   (ha : tendsto a l at_bot) (hb : tendsto b l at_top)
   (h : tendsto (λ i, ∫ x in a i .. b i, ∥f x∥ ∂μ) l (𝓝 I)) :
   integrable f μ :=
 let ⟨I', hI'⟩ := h.is_bounded_under_le in
   integrable_of_interval_integral_norm_bounded I' hfi ha hb hI'
 
-lemma integrable_on_Iic_of_interval_integral_norm_bounded [no_min_order α] (I : ℝ) (b : α)
+lemma integrable_on_Iic_of_interval_integral_norm_bounded (I b : ℝ)
   (hfi : ∀ i, integrable_on f (Ioc (a i) b) μ) (ha : tendsto a l at_bot)
   (h : ∀ᶠ i in l, (∫ x in a i .. b, ∥f x∥ ∂μ) ≤ I) :
   integrable_on f (Iic b) μ :=
@@ -442,14 +439,14 @@ begin
   exact id
 end
 
-lemma integrable_on_Iic_of_interval_integral_norm_tendsto [no_min_order α] (I : ℝ) (b : α)
+lemma integrable_on_Iic_of_interval_integral_norm_tendsto (I b : ℝ)
   (hfi : ∀ i, integrable_on f (Ioc (a i) b) μ) (ha : tendsto a l at_bot)
   (h : tendsto (λ i, ∫ x in a i .. b, ∥f x∥ ∂μ) l (𝓝 I)) :
   integrable_on f (Iic b) μ :=
 let ⟨I', hI'⟩ := h.is_bounded_under_le in
   integrable_on_Iic_of_interval_integral_norm_bounded I' b hfi ha hI'
 
-lemma integrable_on_Ioi_of_interval_integral_norm_bounded (I : ℝ) (a : α)
+lemma integrable_on_Ioi_of_interval_integral_norm_bounded (I a : ℝ)
   (hfi : ∀ i, integrable_on f (Ioc a (b i)) μ) (hb : tendsto b l at_top)
   (h : ∀ᶠ i in l, (∫ x in a .. b i, ∥f x∥ ∂μ) ≤ I) :
   integrable_on f (Ioi a) μ :=
@@ -466,7 +463,7 @@ begin
   exact id
 end
 
-lemma integrable_on_Ioi_of_interval_integral_norm_tendsto (I : ℝ) (a : α)
+lemma integrable_on_Ioi_of_interval_integral_norm_tendsto (I a : ℝ)
   (hfi : ∀ i, integrable_on f (Ioc a (b i)) μ) (hb : tendsto b l at_top)
   (h : tendsto (λ i, ∫ x in a .. b i, ∥f x∥ ∂μ) l (𝓝 $ I)) :
   integrable_on f (Ioi a) μ :=
@@ -477,28 +474,25 @@ end integrable_of_interval_integral
 
 section integral_of_interval_integral
 
-variables {α ι E : Type*}
-          [topological_space α] [linear_order α] [order_closed_topology α]
-          [measurable_space α] [opens_measurable_space α] {μ : measure α}
+variables {ι E : Type*} {μ : measure ℝ}
           {l : filter ι} [is_countably_generated l]
           [measurable_space E] [normed_group E] [normed_space ℝ E] [borel_space E]
           [complete_space E] [second_countable_topology E]
-          {a b : ι → α} {f : α → E}
+          {a b : ι → ℝ} {f : ℝ → E}
 
-lemma interval_integral_tendsto_integral [no_min_order α] [nonempty α]
+lemma interval_integral_tendsto_integral
   (hfi : integrable f μ) (ha : tendsto a l at_bot) (hb : tendsto b l at_top) :
   tendsto (λ i, ∫ x in a i .. b i, f x ∂μ) l (𝓝 $ ∫ x, f x ∂μ) :=
 begin
   let φ := λ i, Ioc (a i) (b i),
-  let c : α := classical.choice ‹_›,
   have hφ : ae_cover μ l φ := ae_cover_Ioc ha hb,
   refine (hφ.integral_tendsto_of_countably_generated hfi).congr' _,
-  filter_upwards [ha.eventually (eventually_le_at_bot c), hb.eventually (eventually_ge_at_top c)]
+  filter_upwards [ha.eventually (eventually_le_at_bot 0), hb.eventually (eventually_ge_at_top 0)]
     with i hai hbi,
   exact (interval_integral.integral_of_le (hai.trans hbi)).symm
 end
 
-lemma interval_integral_tendsto_integral_Iic [no_min_order α] (b : α)
+lemma interval_integral_tendsto_integral_Iic (b : ℝ)
   (hfi : integrable_on f (Iic b) μ) (ha : tendsto a l at_bot) :
   tendsto (λ i, ∫ x in a i .. b, f x ∂μ) l (𝓝 $ ∫ x in Iic b, f x ∂μ) :=
 begin
@@ -510,7 +504,7 @@ begin
   refl,
 end
 
-lemma interval_integral_tendsto_integral_Ioi (a : α)
+lemma interval_integral_tendsto_integral_Ioi (a : ℝ)
   (hfi : integrable_on f (Ioi a) μ) (hb : tendsto b l at_top) :
   tendsto (λ i, ∫ x in a .. b i, f x ∂μ) l (𝓝 $ ∫ x in Ioi a, f x ∂μ) :=
 begin