refactor: change notation for interval integrals

archive/wiedijk_100_theorems/area_of_a_circle.lean

@@ -25,7 +25,7 @@ calculating is indeed measurable and our result is therefore meaningful.
 
 In the main proof, `area_disc`, we use `volume_region_between_eq_integral` followed by
 `interval_integral.integral_of_le` to reduce our goal to a single `interval_integral`:
-  `∫ (x : ℝ) in -r..r, 2 * sqrt (r ^ 2 - x ^ 2) = π * r ^ 2`.
+  `∫_{-r}^{r} x, 2 * sqrt (r ^ 2 - x ^ 2) = π * r ^ 2`.
 After disposing of the trivial case `r = 0`, we show that `λ x, 2 * sqrt (r ^ 2 - x ^ 2)` is equal
 to the derivative of `λ x, r ^ 2 * arcsin (x / r) + x * sqrt (r ^ 2 - x ^ 2)` everywhere on
 `Ioo (-r) r` and that those two functions are continuous, then apply the second fundamental theorem
@@ -81,15 +81,15 @@ begin
   let f := λ x, sqrt (r ^ 2 - x ^ 2),
   let F := λ x, (r:ℝ) ^ 2 * arcsin (r⁻¹ * x) + x * sqrt (r ^ 2 - x ^ 2),
   have hf : continuous f := by continuity,
-  suffices : ∫ x in -r..r, 2 * f x = nnreal.pi * r ^ 2,
+  suffices : ∫_{-r}^{r} x, 2 * f x = nnreal.pi * r ^ 2,
   { have h : integrable_on f (Ioc (-r) r) :=
       hf.integrable_on_Icc.mono_set Ioc_subset_Icc_self,
     calc  volume (disc r)
         = volume (region_between (λ x, -f x) f (Ioc (-r) r)) : by rw disc_eq_region_between
     ... = ennreal.of_real (∫ x in Ioc (-r:ℝ) r, (f - has_neg.neg ∘ f) x) :
           volume_region_between_eq_integral
             h.neg h measurable_set_Ioc (λ x hx, neg_le_self (sqrt_nonneg _))
-    ... = ennreal.of_real (∫ x in (-r:ℝ)..r, 2 * f x) : by simp [two_mul, integral_of_le]
+    ... = ennreal.of_real (∫_{-r}^{r} x, 2 * f x) : by simp [two_mul, integral_of_le]
     ... = nnreal.pi * r ^ 2 : by rw_mod_cast [this, ← ennreal.coe_nnreal_eq], },
   obtain ⟨hle, (heq | hlt)⟩ := ⟨nnreal.coe_nonneg r, hle.eq_or_lt⟩, { simp [← heq] },
   have hderiv : ∀ x ∈ Ioo (-r:ℝ) r, has_deriv_at F (2 * f x) x,
@@ -112,7 +112,7 @@ begin
                    ... = 1 : inv_mul_cancel hlt.ne' },
     { nlinarith } },
   have hcont := (by continuity : continuous F).continuous_on,
-  calc  ∫ x in -r..r, 2 * f x
+  calc  ∫_{-r}^{r} x, 2 * f x
       = F r - F (-r) : integral_eq_sub_of_has_deriv_at_of_le (neg_le_self r.2)
                          hcont hderiv (continuous_const.mul hf).continuous_on.interval_integrable
   ... = nnreal.pi * r ^ 2 : by norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π],

src/analysis/ODE/picard_lindelof.lean

@@ -229,7 +229,7 @@ that the fixed point of this map is the solution of the corresponding ODE.
 
 More precisely, some iteration of this map is a contracting map. -/
 def next (f : fun_space v) : fun_space v :=
-{ to_fun := λ t, v.x₀ + ∫ τ : ℝ in v.t₀..t, f.v_comp τ,
+{ to_fun := λ t, v.x₀ + ∫_{v.t₀}^{t} τ, f.v_comp τ,
   map_t₀' := by rw [integral_same, add_zero],
   lipschitz' := lipschitz_with.of_dist_le_mul $ λ t₁ t₂,
     begin
@@ -239,15 +239,15 @@ def next (f : fun_space v) : fun_space v :=
       exact norm_integral_le_of_norm_le_const (λ t ht, f.norm_v_comp_le _),
     end }
 
-lemma next_apply (t : Icc v.t_min v.t_max) : f.next t = v.x₀ + ∫ τ : ℝ in v.t₀..t, f.v_comp τ := rfl
+lemma next_apply (t : Icc v.t_min v.t_max) : f.next t = v.x₀ + ∫_{v.t₀}^{t} τ, f.v_comp τ := rfl
 
 lemma has_deriv_within_at_next (t : Icc v.t_min v.t_max) :
   has_deriv_within_at (f.next ∘ v.proj) (v t (f t)) (Icc v.t_min v.t_max) t :=
 begin
   haveI : fact ((t : ℝ) ∈ Icc v.t_min v.t_max) := ⟨t.2⟩,
   simp only [(∘), next_apply],
   refine has_deriv_within_at.const_add _ _,
-  have : has_deriv_within_at (λ t : ℝ, ∫ τ in v.t₀..t, f.v_comp τ) (f.v_comp t)
+  have : has_deriv_within_at (λ t : ℝ, ∫_{v.t₀}^{t} τ, f.v_comp τ) (f.v_comp t)
     (Icc v.t_min v.t_max) t,
     from integral_has_deriv_within_at_right (f.interval_integrable_v_comp _ _)
       (f.continuous_v_comp.strongly_measurable_at_filter _ _)

src/analysis/calculus/parametric_interval_integral.lean

@@ -27,7 +27,7 @@ variables {𝕜 : Type*} [is_R_or_C 𝕜] {μ : measure ℝ}
 
 namespace interval_integral
 
-/-- Differentiation under integral of `x ↦ ∫ t in a..b, F x t` at a given point `x₀`, assuming
+/-- Differentiation under integral of `x ↦ ∫_{a}^{b} t, 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₀`. -/
@@ -40,7 +40,7 @@ lemma has_fderiv_at_integral_of_dominated_loc_of_lip {F : H → ℝ → E} {F' :
   (bound_integrable : interval_integrable bound μ a b)
   (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → has_fderiv_at (λ x, F x t) (F' t) x₀) :
   interval_integrable F' μ a b ∧
-    has_fderiv_at (λ x, ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀ :=
+    has_fderiv_at (λ x, ∫_{a}^{b} t, F x t ∂μ) (∫_{a}^{b} t, F' t ∂μ) x₀ :=
 begin
   simp only [interval_integrable_iff, interval_integral_eq_integral_uIoc,
     ← ae_restrict_iff' measurable_set_uIoc] at *,
@@ -61,7 +61,7 @@ lemma has_fderiv_at_integral_of_dominated_of_fderiv_le {F : H → ℝ → E} {F'
   (h_bound : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t)
   (bound_integrable : interval_integrable bound μ a b)
   (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, has_fderiv_at (λ x, F x t) (F' x t) x) :
-  has_fderiv_at (λ x, ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' x₀ t ∂μ) x₀ :=
+  has_fderiv_at (λ x, ∫_{a}^{b} t, F x t ∂μ) (∫_{a}^{b} t, F' x₀ t ∂μ) x₀ :=
 begin
   simp only [interval_integrable_iff, interval_integral_eq_integral_uIoc,
     ← ae_restrict_iff' measurable_set_uIoc] at *,
@@ -83,7 +83,7 @@ lemma has_deriv_at_integral_of_dominated_loc_of_lip {F : 𝕜 → ℝ → E} {F'
   (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₀ :=
+    has_deriv_at (λ x, ∫_{a}^{b} t, F x t ∂μ) (∫_{a}^{b} t, F' t ∂μ) x₀ :=
 begin
   simp only [interval_integrable_iff, interval_integral_eq_integral_uIoc,
     ← ae_restrict_iff' measurable_set_uIoc] at *,
@@ -105,7 +105,7 @@ lemma has_deriv_at_integral_of_dominated_loc_of_deriv_le {F : 𝕜 → ℝ → E
   (bound_integrable : interval_integrable bound μ a b)
   (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, has_deriv_at (λ x, F x t) (F' x t) x) :
   (interval_integrable (F' x₀) μ a b) ∧
-    has_deriv_at (λ x, ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' x₀ t ∂μ) x₀ :=
+    has_deriv_at (λ x, ∫_{a}^{b} t, F x t ∂μ) (∫_{a}^{b} t, F' x₀ t ∂μ) x₀ :=
 begin
   simp only [interval_integrable_iff, interval_integral_eq_integral_uIoc,
     ← ae_restrict_iff' measurable_set_uIoc] at *,

src/analysis/complex/cauchy_integral.lean

@@ -168,9 +168,9 @@ lemma integral_boundary_rect_of_has_fderiv_at_real_off_countable (f : ℂ → E)
   (Hd : ∀ x ∈ (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im)) \ s,
     has_fderiv_at f (f' x) x)
   (Hi : integrable_on (λ z, I • f' z 1 - f' z I) ([z.re, w.re] ×ℂ [z.im, w.im])) :
-  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
-    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) =
-    ∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im, I • f' (x + y * I) 1 - f' (x + y * I) I :=
+  (∫_{z.re}^{w.re} x, f (x + z.im * I)) - (∫_{z.re}^{w.re} x, f (x + w.im * I)) +
+    (I • ∫_{z.im}^{w.im} y, f (re w + y * I)) - I • ∫_{z.im}^{w.im} y, f (re z + y * I) =
+    ∫_{z.re}^{w.re} x, ∫_{z.im}^{w.im} y, I • f' (x + y * I) 1 - f' (x + y * I) I :=
 begin
   set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equiv_real_prod_clm.symm,
   have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y), from λ x y, (mk_eq_add_mul_I x y).symm,
@@ -212,9 +212,9 @@ lemma integral_boundary_rect_of_continuous_on_of_has_fderiv_at_real (f : ℂ →
   (Hd : ∀ x ∈ (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im)),
     has_fderiv_at f (f' x) x)
   (Hi : integrable_on (λ z, I • f' z 1 - f' z I) ([z.re, w.re] ×ℂ [z.im, w.im])) :
-  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
-    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) =
-    ∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im, I • f' (x + y * I) 1 - f' (x + y * I) I :=
+  (∫_{z.re}^{w.re} x, f (x + z.im * I)) - (∫_{z.re}^{w.re} x, f (x + w.im * I)) +
+    (I • ∫_{z.im}^{w.im} y, f (re w + y * I)) - I • ∫_{z.im}^{w.im} y, f (re z + y * I) =
+    ∫_{z.re}^{w.re} x, ∫_{z.im}^{w.im} y, I • f' (x + y * I) 1 - f' (x + y * I) I :=
 integral_boundary_rect_of_has_fderiv_at_real_off_countable f f' z w ∅ countable_empty Hc
   (λ x hx, Hd x hx.1) Hi
 
@@ -226,9 +226,9 @@ over the rectangle. -/
 lemma integral_boundary_rect_of_differentiable_on_real (f : ℂ → E) (z w : ℂ)
   (Hd : differentiable_on ℝ f ([z.re, w.re] ×ℂ [z.im, w.im]))
   (Hi : integrable_on (λ z, I • fderiv ℝ f z 1 - fderiv ℝ f z I) ([z.re, w.re] ×ℂ [z.im, w.im])) :
-  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
-    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) =
-    ∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im,
+  (∫_{z.re}^{w.re} x, f (x + z.im * I)) - (∫_{z.re}^{w.re} x, f (x + w.im * I)) +
+    (I • ∫_{z.im}^{w.im} y, f (re w + y * I)) - I • ∫_{z.im}^{w.im} y, f (re z + y * I) =
+    ∫_{z.re}^{w.re} x, ∫_{z.im}^{w.im} y,
       I • fderiv ℝ f (x + y * I) 1 - fderiv ℝ f (x + y * I) I :=
 integral_boundary_rect_of_has_fderiv_at_real_off_countable f (fderiv ℝ f) z w ∅ countable_empty
   Hd.continuous_on
@@ -243,9 +243,9 @@ lemma integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (f : ℂ
   (z w : ℂ) (s : set ℂ) (hs : s.countable) (Hc : continuous_on f ([z.re, w.re] ×ℂ [z.im, w.im]))
   (Hd : ∀ x ∈ (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im)) \ s,
     differentiable_at ℂ f x) :
-  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
-    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
-      I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) = 0 :=
+  (∫_{z.re}^{w.re} x, f (x + z.im * I)) - (∫_{z.re}^{w.re} x, f (x + w.im * I)) +
+    (I • ∫_{z.im}^{w.im} y, f (re w + y * I)) -
+      I • ∫_{z.im}^{w.im} y, f (re z + y * I) = 0 :=
 by refine (integral_boundary_rect_of_has_fderiv_at_real_off_countable f
   (λ z, (fderiv ℂ f z).restrict_scalars ℝ) z w s hs Hc
   (λ x hx, (Hd x hx).has_fderiv_at.restrict_scalars ℝ) _).trans _;
@@ -259,9 +259,9 @@ lemma integral_boundary_rect_eq_zero_of_continuous_on_of_differentiable_on (f :
   (Hc : continuous_on f ([z.re, w.re] ×ℂ [z.im, w.im]))
   (Hd : differentiable_on ℂ f
     (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im))) :
-  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
-    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
-      I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) = 0 :=
+  (∫_{z.re}^{w.re} x, f (x + z.im * I)) - (∫_{z.re}^{w.re} x, f (x + w.im * I)) +
+    (I • ∫_{z.im}^{w.im} y, f (re w + y * I)) -
+      I • ∫_{z.im}^{w.im} y, f (re z + y * I) = 0 :=
 integral_boundary_rect_eq_zero_of_differentiable_on_off_countable f z w ∅ countable_empty
   Hc $ λ x hx, Hd.differentiable_at $ (is_open_Ioo.re_prod_im is_open_Ioo).mem_nhds hx.1
 
@@ -270,9 +270,9 @@ over the boundary of a rectangle equals zero. More precisely, if `f` is complex
 closed rectangle, then its integral over the boundary of the rectangle equals zero. -/
 lemma integral_boundary_rect_eq_zero_of_differentiable_on (f : ℂ → E) (z w : ℂ)
   (H : differentiable_on ℂ f ([z.re, w.re] ×ℂ [z.im, w.im])) :
-  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
-    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
-      I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) = 0 :=
+  (∫_{z.re}^{w.re} x, f (x + z.im * I)) - (∫_{z.re}^{w.re} x, f (x + w.im * I)) +
+    (I • ∫_{z.im}^{w.im} y, f (re w + y * I)) -
+      I • ∫_{z.im}^{w.im} y, f (re z + y * I) = 0 :=
 integral_boundary_rect_eq_zero_of_continuous_on_of_differentiable_on f z w H.continuous_on $
   H.mono $
     inter_subset_inter (preimage_mono Ioo_subset_Icc_self) (preimage_mono Ioo_subset_Icc_self)
@@ -294,8 +294,8 @@ begin
   obtain ⟨b, rfl⟩ : ∃ b, real.exp b = R, from ⟨real.log R, real.exp_log (h0.trans_le hle)⟩,
   rw [real.exp_le_exp] at hle,
   -- Unfold definition of `circle_integral` and cancel some terms.
-  suffices : ∫ θ in 0..2 * π, I • f (circle_map c (real.exp b) θ) =
-    ∫ θ in 0..2 * π, I • f (circle_map c (real.exp a) θ),
+  suffices : ∫_{0}^{2 * π} θ, I • f (circle_map c (real.exp b) θ) =
+    ∫_{0}^{2 * π} θ, I • f (circle_map c (real.exp a) θ),
     by simpa only [circle_integral, add_sub_cancel', of_real_exp, ← exp_add, smul_smul,
       ← div_eq_mul_inv, mul_div_cancel_left _ (circle_map_ne_center (real.exp_pos _).ne'),
       circle_map_sub_center, deriv_circle_map],

src/analysis/convolution.lean

@@ -1576,10 +1576,10 @@ variables [normed_space ℝ E] [normed_space ℝ E'] [normed_space ℝ F] [compl
 
 /-- The forward convolution of two functions `f` and `g` on `ℝ`, with respect to a continuous
 bilinear map `L` and measure `ν`. It is defined to be the function mapping `x` to
-`∫ t in 0..x, L (f t) (g (x - t)) ∂ν` if `0 < x`, and 0 otherwise. -/
+`∫_{0}^{x} t, L (f t) (g (x - t)) ∂ν` if `0 < x`, and 0 otherwise. -/
 noncomputable def pos_convolution
   (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F) (ν : measure ℝ . volume_tac) : ℝ → F :=
-indicator (Ioi (0:ℝ)) (λ x, ∫ t in 0..x, L (f t) (g (x - t)) ∂ν)
+indicator (Ioi (0:ℝ)) (λ x, ∫_{0}^{x} t, L (f t) (g (x - t)) ∂ν)
 
 lemma pos_convolution_eq_convolution_indicator
   (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F) (ν : measure ℝ . volume_tac) [has_no_atoms ν] :
@@ -1631,7 +1631,7 @@ lemma integral_pos_convolution [complete_space E] [complete_space E'] {μ ν : m
   [sigma_finite μ] [sigma_finite ν] [is_add_right_invariant μ] [has_no_atoms ν]
   {f : ℝ → E} {g : ℝ → E'} (hf : integrable_on f (Ioi 0) ν)
   (hg : integrable_on g (Ioi 0) μ) (L : E →L[ℝ] E' →L[ℝ] F)  :
-  ∫ x:ℝ in Ioi 0, (∫ t:ℝ in 0..x, L (f t) (g (x - t)) ∂ν) ∂μ =
+  ∫ x:ℝ in Ioi 0, (∫_{0}^{x} t:ℝ, L (f t) (g (x - t)) ∂ν) ∂μ =
     L (∫ x:ℝ in Ioi 0, f x ∂ν) (∫ x:ℝ in Ioi 0, g x ∂μ) :=
 begin
   rw ←integrable_indicator_iff (measurable_set_Ioi : measurable_set (Ioi (0:ℝ))) at hf hg,

src/analysis/fourier/add_circle.lean

@@ -311,7 +311,7 @@ def fourier_coeff (f : add_circle T → E) (n : ℤ) : E :=
 /-- The Fourier coefficients of a function on `add_circle T` can be computed as an integral
 over `[a, a + T]`, for any real `a`. -/
 lemma fourier_coeff_eq_interval_integral (f : add_circle T → E) (n : ℤ) (a : ℝ) :
-  fourier_coeff f n = (1 / T) • ∫ x in a .. a + T, @fourier T (-n) x • f x :=
+  fourier_coeff f n = (1 / T) • ∫_{a}^{a + T} x, @fourier T (-n) x • f x :=
 begin
   have : ∀ (x : ℝ), @fourier T (-n) x • f x = (λ (z : add_circle T), @fourier T (-n) z • f z) x,
   { intro x, refl, },
@@ -342,7 +342,7 @@ end
 
 lemma fourier_coeff_on_eq_integral {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b) :
   fourier_coeff_on hab f n =
-  (1 / (b - a)) • ∫ x in a ..b, fourier (-n) (x : add_circle (b - a)) • f x :=
+  (1 / (b - a)) • ∫_{a}^{b} x, fourier (-n) (x : add_circle (b - a)) • f x :=
 begin
   rw [fourier_coeff_on, fourier_coeff_eq_interval_integral _ _ a],
   congr' 1,

src/analysis/fourier/poisson_summation.lean

@@ -66,21 +66,21 @@ begin
     simpa only [mul_one] using this.int_mul n x },
   -- Now the main argument. First unwind some definitions.
   calc fourier_coeff (periodic.lift $ f.periodic_tsum_comp_add_zsmul 1) m
-  = ∫ x in 0..1, e x * (∑' n : ℤ, f.comp (continuous_map.add_right n)) x :
+  = ∫_{0}^{1} x, e x * (∑' n : ℤ, f.comp (continuous_map.add_right n)) x :
     by simp_rw [fourier_coeff_eq_interval_integral _ m 0, div_one, one_smul, zero_add, comp_apply,
       coe_mk, periodic.lift_coe, zsmul_one, smul_eq_mul]
   -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
-  ... = ∫ x in 0..1, (∑' n : ℤ, (e * f.comp (continuous_map.add_right n)) x) :
+  ... = ∫_{0}^{1} x, (∑' n : ℤ, (e * f.comp (continuous_map.add_right n)) x) :
     by simp_rw [coe_mul, pi.mul_apply, ←tsum_apply (summable_of_locally_summable_norm hf),
       tsum_mul_left]
   -- Swap sum and integral.
-  ... = ∑' n : ℤ, ∫ x in 0..1, (e * f.comp (continuous_map.add_right n)) x :
+  ... = ∑' n : ℤ, ∫_{0}^{1} x, (e * f.comp (continuous_map.add_right n)) x :
     begin
       refine (interval_integral.tsum_interval_integral_eq_of_summable_norm _).symm,
       convert hf ⟨uIcc 0 1, is_compact_uIcc⟩,
       exact funext (λ n, neK _ _)
     end
-  ... = ∑' n : ℤ, ∫ x in 0..1, (e * f).comp (continuous_map.add_right n) x :
+  ... = ∑' n : ℤ, ∫_{0}^{1} x, (e * f).comp (continuous_map.add_right n) x :
     begin
       simp only [continuous_map.comp_apply, mul_comp] at eadd ⊢,
       simp_rw eadd,

src/analysis/normed_space/triv_sq_zero_ext.lean

@@ -28,7 +28,7 @@ For now, this file contains results about `exp` for this type.
   like `exp_add`.
 * Generalize more of these results to non-commutative `R`. In principle, under sufficient conditions
   we should expect
- `(exp 𝕜 x).snd = ∫ t in 0..1, exp 𝕜 (t • x.fst) • op (exp 𝕜 ((1 - t) • x.fst)) • x.snd`
+ `(exp 𝕜 x).snd = ∫_{0}^{1} t, exp 𝕜 (t • x.fst) • op (exp 𝕜 ((1 - t) • x.fst)) • x.snd`
   ([Physics.SE](https://physics.stackexchange.com/a/41671/185147), and
   https://link.springer.com/chapter/10.1007/978-3-540-44953-9_2).
 

src/analysis/special_functions/gamma/basic.lean

@@ -151,7 +151,7 @@ namespace complex
 section Gamma_recurrence
 
 /-- The indefinite version of the `Γ` function, `Γ(s, X) = ∫ x ∈ 0..X, exp(-x) x ^ (s - 1)`. -/
-def partial_Gamma (s : ℂ) (X : ℝ) : ℂ := ∫ x in 0..X, (-x).exp * x ^ (s - 1)
+def partial_Gamma (s : ℂ) (X : ℝ) : ℂ := ∫_{0}^{X} x, (-x).exp * x ^ (s - 1)
 
 lemma tendsto_partial_Gamma {s : ℂ} (hs: 0 < s.re) :
   tendsto (λ X:ℝ, partial_Gamma s X) at_top (𝓝 $ Gamma_integral s) :=