α : Type u_1
E : Type u_2
F : Type ?u.99640
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
⊢ (∫ (a : α), inner (↑↑(f + f') a) (↑↑g a) ∂μ) = ∫ (a : α), inner (↑↑f a + ↑↑f' a) (↑↑g a) ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.99640
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
⊢ inner (f + f') g = inner f g + inner f' g
simp_rw [inner_def, ← integral_add (integrable_inner f g) (integrable_inner f' g), ←
  inner_add_left]
α : Type u_1
E : Type u_2
F : Type ?u.99640
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ (fun a => inner (↑↑(f + f') a) (↑↑g a)) x = (fun a => inner (↑↑f a + ↑↑f' a) (↑↑g a)) x
α : Type u_1
E : Type u_2
F : Type ?u.99640
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
⊢ (∫ (a : α), inner (↑↑(f + f') a) (↑↑g a) ∂μ) = ∫ (a : α), inner (↑↑f a + ↑↑f' a) (↑↑g a) ∂μ
refine' integral_congr_ae ((coeFn_add f f').mono fun x hx => _)
α : Type u_1
E : Type u_2
F : Type ?u.99640
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ inner (↑↑(f + f') x) (↑↑g x) = inner (↑↑f x + ↑↑f' x) (↑↑g x)
α : Type u_1
E : Type u_2
F : Type ?u.99640
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ (fun a => inner (↑↑(f + f') a) (↑↑g a)) x = (fun a => inner (↑↑f a + ↑↑f' a) (↑↑g a)) x
simp only
no goals
α : Type u_1
E : Type u_2
F : Type ?u.99640
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ inner (↑↑(f + f') x) (↑↑g x) = inner (↑↑f x + ↑↑f' x) (↑↑g x)
rw [hx, Pi.add_apply]