α : Type u_1
E : Type u_2
F : Type ?u.103781
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
⊢ (∫ (a : α), inner (↑↑(r • f) a) (↑↑g a) ∂μ) = ∫ (a : α), ↑(starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a) ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.103781
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
⊢ inner (r • f) g = ↑(starRingEnd 𝕜) r * inner f g
rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul]
α : Type u_1
E : Type u_2
F : Type ?u.103781
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ (fun a => inner (↑↑(r • f) a) (↑↑g a)) x = (fun a => ↑(starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a)) x
α : Type u_1
E : Type u_2
F : Type ?u.103781
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
⊢ (∫ (a : α), inner (↑↑(r • f) a) (↑↑g a) ∂μ) = ∫ (a : α), ↑(starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a) ∂μ
refine' integral_congr_ae ((coeFn_smul r f).mono fun x hx => _)
α : Type u_1
E : Type u_2
F : Type ?u.103781
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ inner (↑↑(r • f) x) (↑↑g x) = ↑(starRingEnd 𝕜) r • inner (↑↑f x) (↑↑g x)
α : Type u_1
E : Type u_2
F : Type ?u.103781
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ (fun a => inner (↑↑(r • f) a) (↑↑g a)) x = (fun a => ↑(starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a)) x
simp only
no goals
α : Type u_1
E : Type u_2
F : Type ?u.103781
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ inner (↑↑(r • f) x) (↑↑g x) = ↑(starRingEnd 𝕜) r • inner (↑↑f x) (↑↑g x)
rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]