case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ↑(weightedSMul (μ + ν) s) x = ↑(weightedSMul μ s + weightedSMul ν s) x
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
ext1 x
case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ↑(weightedSMul (μ + ν) s) x = (↑(weightedSMul μ s) + ↑(weightedSMul ν s)) x
case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ↑(weightedSMul (μ + ν) s) x = ↑(weightedSMul μ s + weightedSMul ν s) x
push_cast
case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ENNReal.toReal (↑↑(μ + ν) s) • x = ENNReal.toReal (↑↑μ s) • x + ENNReal.toReal (↑↑ν s) • x
case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ↑(weightedSMul (μ + ν) s) x = (↑(weightedSMul μ s) + ↑(weightedSMul ν s)) x
simp_rw [Pi.add_apply, weightedSMul_apply]
case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ENNReal.toReal ((↑↑μ + ↑↑ν) s) • x = ENNReal.toReal (↑↑μ s) • x + ENNReal.toReal (↑↑ν s) • x
case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ENNReal.toReal (↑↑(μ + ν) s) • x = ENNReal.toReal (↑↑μ s) • x + ENNReal.toReal (↑↑ν s) • x
push_cast
no goals
case h
α : Type u_1
E : Type ?u.23178
F : Type u_2
𝕜 : Type ?u.23184
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : ↑↑μ s ≠ ⊤
hνs : ↑↑ν s ≠ ⊤
x : F
⊢ ENNReal.toReal ((↑↑μ + ↑↑ν) s) • x = ENNReal.toReal (↑↑μ s) • x + ENNReal.toReal (↑↑ν s) • x
rw [Pi.add_apply, ENNReal.toReal_add hμs hνs, add_smul]