α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : { x // x ∈ Lp E 1 }
⊢ setToL1 hT' = c • setToL1 hT
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : { x // x ∈ Lp E 1 }
⊢ ↑(setToL1 hT') f = c • ↑(setToL1 hT) f
suffices setToL1 hT' = c • setToL1 hT by rw [this, ContinuousLinearMap.smul_apply]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : { x // x ∈ Lp E 1 }
⊢ ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ) = setToL1SCLM α E μ hT'
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : { x // x ∈ Lp E 1 }
⊢ setToL1 hT' = c • setToL1 hT
refine' ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT') _ _ _ _ _
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ↑(ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ)) f = ↑(setToL1SCLM α E μ hT') f
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : { x // x ∈ Lp E 1 }
⊢ ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ) = setToL1SCLM α E μ hT'
ext1 f
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ↑(ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ)) f = ↑(setToL1SCLM α E μ hT') f
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ↑(ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ)) f = ↑(setToL1SCLM α E μ hT') f
simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.smul_comp,
  Pi.smul_apply, ContinuousLinearMap.coe_smul']
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
⊢ c • ↑(setToL1 hT) ↑f = ↑(setToL1SCLM α E μ hT') f
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ↑(ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ)) f = ↑(setToL1SCLM α E μ hT') f
suffices c • setToL1 hT f = setToL1SCLM α E μ hT' f by rw [← this]; congr
no goals
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
⊢ c • ↑(setToL1 hT) ↑f = ↑(setToL1SCLM α E μ hT') f
rw [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left' c hT hT' h_smul]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : { x // x ∈ Lp E 1 }
this : setToL1 hT' = c • setToL1 hT
⊢ ↑(setToL1 hT') f = c • ↑(setToL1 hT) f
rw [this, ContinuousLinearMap.smul_apply]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
this : c • ↑(setToL1 hT) ↑f = ↑(setToL1SCLM α E μ hT') f
⊢ ↑(ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ)) f = c • ↑(setToL1 hT) ↑f
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
this : c • ↑(setToL1 hT) ↑f = ↑(setToL1SCLM α E μ hT') f
⊢ ↑(ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ)) f = ↑(setToL1SCLM α E μ hT') f
rw [← this]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1139564
G : Type ?u.1139567
𝕜 : Type ?u.1139570
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f✝ : { x // x ∈ Lp E 1 }
f : { x // x ∈ simpleFunc E 1 μ }
this : c • ↑(setToL1 hT) ↑f = ↑(setToL1SCLM α E μ hT') f
⊢ ↑(ContinuousLinearMap.comp (c • setToL1 hT) (coeToLp α E ℝ)) f = c • ↑(setToL1 hT) ↑f
congr