case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)

case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
by_cases hc'0 : c' = 0
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ ∀ (b : { x // x ∈ Lp G 1 }) (ε : ℝ),
    ε > 0 →
      ∃ δ,
        δ > 0 ∧
          ∀ (a : { x // x ∈ Lp G 1 }),
            dist a b < δ →
              dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑b (_ : Integrable ↑↑b)) < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
rw [Metric.continuous_iff]
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (a : { x // x ∈ Lp G 1 }),
        dist a f < δ → dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ ∀ (b : { x // x ∈ Lp G 1 }) (ε : ℝ),
    ε > 0 →
      ∃ δ,
        δ > 0 ∧
          ∀ (a : { x // x ∈ Lp G 1 }),
            dist a b < δ →
              dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑b (_ : Integrable ↑↑b)) < ε
intro f ε hε_pos
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
⊢ ε / 2 / ENNReal.toReal c' > 0 ∧
    ∀ (a : { x // x ∈ Lp G 1 }),
      dist a f < ε / 2 / ENNReal.toReal c' →
        dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (a : { x // x ∈ Lp G 1 }),
        dist a f < δ → dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
use ε / 2 / c'.toReal
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
⊢ ∀ (a : { x // x ∈ Lp G 1 }),
    dist a f < ε / 2 / ENNReal.toReal c' →
      dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
⊢ ε / 2 / ENNReal.toReal c' > 0 ∧
    ∀ (a : { x // x ∈ Lp G 1 }),
      dist a f < ε / 2 / ENNReal.toReal c' →
        dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
refine' ⟨div_pos (half_pos hε_pos) (toReal_pos hc'0 hc'), _⟩
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : dist g f < ε / 2 / ENNReal.toReal c'
⊢ dist (Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
⊢ ∀ (a : { x // x ∈ Lp G 1 }),
    dist a f < ε / 2 / ENNReal.toReal c' →
      dist (Integrable.toL1 ↑↑a (_ : Integrable ↑↑a)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
intro g hfg
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
⊢ ENNReal.toReal
      (snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ') <
    ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : dist g f < ε / 2 / ENNReal.toReal c'
⊢ dist (Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) (Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) < ε
rw [Lp.dist_def] at hfg ⊢
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
⊢ ENNReal.toReal
      (snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ') <
    ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
⊢ ENNReal.toReal
      (snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ') <
    ε
let h_int := fun f' : α →₁[μ] G => (L1.integrable_coeFn f').of_measure_le_smul c' hc' hμ'_le
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
⊢ ENNReal.toReal
      (snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ') <
    ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
⊢ ENNReal.toReal
      (snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ') <
    ε
have :
  snorm (⇑(Integrable.toL1 g (h_int g)) - ⇑(Integrable.toL1 f (h_int f))) 1 μ' =
    snorm (⇑g - ⇑f) 1 μ' :=
  snorm_congr_ae ((Integrable.coeFn_toL1 _).sub (Integrable.coeFn_toL1 _))
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
⊢ ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ') < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
⊢ ENNReal.toReal
      (snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ') <
    ε
rw [this]
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ') < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
⊢ ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ') < ε
have h_snorm_ne_top : snorm (⇑g - ⇑f) 1 μ ≠ ∞ := by
  rw [← snorm_congr_ae (Lp.coeFn_sub _ _)]; exact Lp.snorm_ne_top _
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ') < ε
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ') < ε
have h_snorm_ne_top' : snorm (⇑g - ⇑f) 1 μ' ≠ ∞ := by
  refine' ((snorm_mono_measure _ hμ'_le).trans_lt _).ne
  rw [snorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
  refine' ENNReal.mul_lt_top _ h_snorm_ne_top
  simp [hc', hc'0]
no goals
case neg
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ') < ε
calc
  (snorm (⇑g - ⇑f) 1 μ').toReal ≤ (c' * snorm (⇑g - ⇑f) 1 μ).toReal := by
    rw [toReal_le_toReal h_snorm_ne_top' (ENNReal.mul_ne_top hc' h_snorm_ne_top)]
    refine' (snorm_mono_measure (⇑g - ⇑f) hμ'_le).trans _
    rw [snorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
    simp
  _ = c'.toReal * (snorm (⇑g - ⇑f) 1 μ).toReal := toReal_mul
  _ ≤ c'.toReal * (ε / 2 / c'.toReal) :=
    (mul_le_mul le_rfl hfg.le toReal_nonneg toReal_nonneg)
  _ = ε / 2 := by
    refine' mul_div_cancel' (ε / 2) _; rw [Ne.def, toReal_eq_zero_iff]; simp [hc', hc'0]
  _ < ε := half_lt_self hε_pos
case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
have hμ'0 : μ' = 0 := by rw [← Measure.nonpos_iff_eq_zero']; refine' hμ'_le.trans _; simp [hc'0]
case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
h_im_zero : (fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
have h_im_zero :
  (fun f : α →₁[μ] G =>
      (Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f)).toL1 f) =
    0 := by
  ext1 f; ext1; simp_rw [hμ'0]; simp only [ae_zero, EventuallyEq, eventually_bot]
case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
h_im_zero : (fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) = 0
⊢ Continuous 0
case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
h_im_zero : (fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) = 0
⊢ Continuous fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)
rw [h_im_zero]
no goals
case pos
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
h_im_zero : (fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) = 0
⊢ Continuous 0
exact continuous_zero
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ μ' ≤ 0
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ μ' = 0
rw [← Measure.nonpos_iff_eq_zero']
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ c' • μ ≤ 0
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ μ' ≤ 0
refine' hμ'_le.trans _
no goals
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ c' • μ ≤ 0
simp [hc'0]
case h
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : { x // x ∈ Lp G 1 }
⊢ Integrable.toL1 ↑↑f (_ : Integrable ↑↑f) = OfNat.ofNat 0 f
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
⊢ (fun f => Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) = 0
ext1 f
case h.h
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : { x // x ∈ Lp G 1 }
⊢ ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) =ᵐ[μ'] ↑↑(OfNat.ofNat 0 f)
case h
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : { x // x ∈ Lp G 1 }
⊢ Integrable.toL1 ↑↑f (_ : Integrable ↑↑f) = OfNat.ofNat 0 f
ext1
case h.h
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : { x // x ∈ Lp G 1 }
⊢ ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) =ᵐ[0] ↑↑(OfNat.ofNat 0 f)
case h.h
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : { x // x ∈ Lp G 1 }
⊢ ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) =ᵐ[μ'] ↑↑(OfNat.ofNat 0 f)
simp_rw [hμ'0]
no goals
case h.h
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : { x // x ∈ Lp G 1 }
⊢ ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f)) =ᵐ[0] ↑↑(OfNat.ofNat 0 f)
simp only [ae_zero, EventuallyEq, eventually_bot]
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
⊢ snorm (↑↑(g - f)) 1 μ ≠ ⊤
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
⊢ snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
rw [← snorm_congr_ae (Lp.coeFn_sub _ _)]
no goals
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
⊢ snorm (↑↑(g - f)) 1 μ ≠ ⊤
exact Lp.snorm_ne_top _
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ snorm (↑↑g - ↑↑f) 1 (c' • μ) < ⊤
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
refine' ((snorm_mono_measure _ hμ'_le).trans_lt _).ne
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ c' ^ ENNReal.toReal (1 / 1) * snorm (↑↑g - ↑↑f) 1 μ < ⊤
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ snorm (↑↑g - ↑↑f) 1 (c' • μ) < ⊤
rw [snorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ c' ^ ENNReal.toReal (1 / 1) ≠ ⊤
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ c' ^ ENNReal.toReal (1 / 1) * snorm (↑↑g - ↑↑f) 1 μ < ⊤
refine' ENNReal.mul_lt_top _ h_snorm_ne_top
no goals
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
⊢ c' ^ ENNReal.toReal (1 / 1) ≠ ⊤
simp [hc', hc'0]
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ snorm (↑↑g - ↑↑f) 1 μ' ≤ c' * snorm (↑↑g - ↑↑f) 1 μ
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ') ≤ ENNReal.toReal (c' * snorm (↑↑g - ↑↑f) 1 μ)
rw [toReal_le_toReal h_snorm_ne_top' (ENNReal.mul_ne_top hc' h_snorm_ne_top)]
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ snorm (↑↑g - ↑↑f) 1 (c' • μ) ≤ c' * snorm (↑↑g - ↑↑f) 1 μ
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ snorm (↑↑g - ↑↑f) 1 μ' ≤ c' * snorm (↑↑g - ↑↑f) 1 μ
refine' (snorm_mono_measure (⇑g - ⇑f) hμ'_le).trans _
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ c' ^ ENNReal.toReal (1 / 1) * snorm (↑↑g - ↑↑f) 1 μ ≤ c' * snorm (↑↑g - ↑↑f) 1 μ
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ snorm (↑↑g - ↑↑f) 1 (c' • μ) ≤ c' * snorm (↑↑g - ↑↑f) 1 μ
rw [snorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
no goals
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ c' ^ ENNReal.toReal (1 / 1) * snorm (↑↑g - ↑↑f) 1 μ ≤ c' * snorm (↑↑g - ↑↑f) 1 μ
simp
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ENNReal.toReal c' ≠ 0
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ENNReal.toReal c' * (ε / 2 / ENNReal.toReal c') = ε / 2
refine' mul_div_cancel' (ε / 2) _
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ¬(c' = 0 ∨ c' = ⊤)
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ENNReal.toReal c' ≠ 0
rw [Ne.def, toReal_eq_zero_iff]
no goals
α : Type u_1
E : Type ?u.1624064
F : Type ?u.1624067
F' : Type ?u.1624070
G : Type u_2
𝕜 : Type ?u.1624076
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g✝ : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : { x // x ∈ Lp G 1 }
ε : ℝ
hε_pos : ε > 0
g : { x // x ∈ Lp G 1 }
hfg : ENNReal.toReal (snorm (↑↑g - ↑↑f) 1 μ) < ε / 2 / ENNReal.toReal c'
h_int : ∀ (f' : { x // x ∈ Lp G 1 }), Integrable ↑↑f' :=
  fun f' => Integrable.of_measure_le_smul c' hc' hμ'_le (L1.integrable_coeFn f')
this :
  snorm (↑↑(Integrable.toL1 ↑↑g (_ : Integrable ↑↑g)) - ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))) 1 μ' =
    snorm (↑↑g - ↑↑f) 1 μ'
h_snorm_ne_top : snorm (↑↑g - ↑↑f) 1 μ ≠ ⊤
h_snorm_ne_top' : snorm (↑↑g - ↑↑f) 1 μ' ≠ ⊤
⊢ ¬(c' = 0 ∨ c' = ⊤)
simp [hc', hc'0]