ι : Type ?u.10290574
𝕜 : Type ?u.10290577
E : Type u_1
F : Type ?u.10290583
A : Type ?u.10290586
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ ‖if a ≤ b then 1 else -1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
ι : Type ?u.10290574
𝕜 : Type ?u.10290577
E : Type u_1
F : Type ?u.10290583
A : Type ?u.10290586
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
simp_rw [intervalIntegral_eq_integral_uIoc, norm_smul]
no goals
ι : Type ?u.10290574
𝕜 : Type ?u.10290577
E : Type u_1
F : Type ?u.10290583
A : Type ?u.10290586
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ ‖if a ≤ b then 1 else -1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
split_ifs <;> simp only [norm_neg, norm_one, one_mul]