α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
⊢ DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G)
borelize G
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
⊢ g ∈ closure (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G)
intro g
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
⊢ g ∈ closure (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))
rw [mem_closure_iff_seq_limit]
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have hg_memℒp : Memℒp (g : α → G) p μ := Lp.memℒp (g : Lp G p μ)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have zero_mem : (0 : G) ∈ (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } := by
  simp only [union_singleton, mem_inter_iff, mem_insert_iff, eq_self_iff_true, true_or_iff,
    mem_setOf_eq, le_refl, and_self_iff]
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have : SeparableSpace ((range (g : α → G) ∪ {0}) ∩ { y | 0 ≤ y } : Set G) := by
  apply IsSeparable.separableSpace
  apply IsSeparable.mono _ (Set.inter_subset_left _ _)
  exact
    (Lp.stronglyMeasurable (g : Lp G p μ)).isSeparable_range.union
      (finite_singleton _).isSeparable
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have g_meas : Measurable (g : α → G) := (Lp.stronglyMeasurable (g : Lp G p μ)).measurable
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
let x n := SimpleFunc.approxOn g g_meas ((range (g : α → G) ∪ {0}) ∩ { y | 0 ≤ y }) 0 zero_mem n
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have hx_nonneg : ∀ n, 0 ≤ x n := by
  intro n a
  change x n a ∈ { y : G | 0 ≤ y }
  have A : (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } ⊆ { y | 0 ≤ y } :=
    inter_subset_right _ _
  apply A
  exact SimpleFunc.approxOn_mem g_meas _ n a
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have hx_memℒp : ∀ n, Memℒp (x n) p μ :=
  SimpleFunc.memℒp_approxOn _ hg_memℒp _ ⟨aestronglyMeasurable_const, by simp⟩
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have h_toLp := fun n => Memℒp.coeFn_toLp (hx_memℒp n)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
have hx_nonneg_Lp : ∀ n, 0 ≤ toLp (x n) (hx_memℒp n) := by
  intro n
  rw [← Lp.simpleFunc.coeFn_le, Lp.simpleFunc.toLp_eq_toLp]
  filter_upwards [Lp.simpleFunc.coeFn_zero p μ G, h_toLp n] with a ha0 ha_toLp
  rw [ha0, ha_toLp]
  exact hx_nonneg n a
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto
    (fun n =>
      coeSimpleFuncNonnegToLpNonneg p μ G
        { val := toLp (x n) (_ : Memℒp (↑(x n)) p), property := (_ : 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)) })
    atTop (𝓝 g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
refine'
  ⟨fun n =>
    (coeSimpleFuncNonnegToLpNonneg p μ G) ⟨toLp (x n) (hx_memℒp n), hx_nonneg_Lp n⟩,
    fun n => mem_range_self _, _⟩
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto (fun n => ↑(toLp (x n) (_ : Memℒp (↑(x n)) p))) atTop (𝓝 ↑g)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto
    (fun n =>
      coeSimpleFuncNonnegToLpNonneg p μ G
        { val := toLp (x n) (_ : Memℒp (↑(x n)) p), property := (_ : 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)) })
    atTop (𝓝 g)
suffices Tendsto (fun n : ℕ => (toLp (x n) (hx_memℒp n) : Lp G p μ)) atTop (𝓝 (g : Lp G p μ)) by
  rw [tendsto_iff_dist_tendsto_zero] at this ⊢
  simp_rw [Subtype.dist_eq]
  exact this
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto (fun n => snorm (↑↑↑(toLp (x n) (_ : Memℒp (↑(x n)) p)) - ↑↑↑g) p μ) atTop (𝓝 0)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto (fun n => ↑(toLp (x n) (_ : Memℒp (↑(x n)) p))) atTop (𝓝 ↑g)
rw [Lp.tendsto_Lp_iff_tendsto_ℒp']
case refine_1
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x_1 => ↑(x n) x_1) =ᵐ[μ] fun x_1 => ↑↑↑(toLp (x n) (_ : Memℒp (↑(x n)) p)) x_1

case refine_2
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x => ↑↑↑g x) =ᵐ[μ] fun x => ↑↑↑g x
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto (fun n => snorm (↑↑↑(toLp (x n) (_ : Memℒp (↑(x n)) p)) - ↑↑↑g) p μ) atTop (𝓝 0)
refine Filter.Tendsto.congr (fun n => snorm_congr_ae (EventuallyEq.sub ?_ ?_)) hx_tendsto
no goals
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
⊢ 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
simp only [union_singleton, mem_inter_iff, mem_insert_iff, eq_self_iff_true, true_or_iff,
  mem_setOf_eq, le_refl, and_self_iff]
case hs
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ IsSeparable ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
apply IsSeparable.separableSpace
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ IsSeparable (Set.range ↑↑↑g ∪ {0})
case hs
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ IsSeparable ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
apply IsSeparable.mono _ (Set.inter_subset_left _ _)
no goals
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ IsSeparable (Set.range ↑↑↑g ∪ {0})
exact
  (Lp.stronglyMeasurable (g : Lp G p μ)).isSeparable_range.union
    (finite_singleton _).isSeparable
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
⊢ ↑0 a ≤ ↑(x n) a
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
⊢ ∀ (n : ℕ), 0 ≤ x n
intro n a
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
⊢ ↑(x n) a ∈ {y | 0 ≤ y}
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
⊢ ↑0 a ≤ ↑(x n) a
change x n a ∈ { y : G | 0 ≤ y }
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
A : (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y} ⊆ {y | 0 ≤ y}
⊢ ↑(x n) a ∈ {y | 0 ≤ y}
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
⊢ ↑(x n) a ∈ {y | 0 ≤ y}
have A : (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } ⊆ { y | 0 ≤ y } :=
  inter_subset_right _ _
case a
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
A : (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y} ⊆ {y | 0 ≤ y}
⊢ ↑(x n) a ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
A : (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y} ⊆ {y | 0 ≤ y}
⊢ ↑(x n) a ∈ {y | 0 ≤ y}
apply A
no goals
case a
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
A : (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y} ⊆ {y | 0 ≤ y}
⊢ ↑(x n) a ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
exact SimpleFunc.approxOn_mem g_meas _ n a
no goals
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
⊢ snorm (fun x => 0) p μ < ⊤
simp
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
⊢ 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
⊢ ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
intro n
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
⊢ ↑↑↑0 ≤ᵐ[μ] ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p))
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
⊢ 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
rw [← Lp.simpleFunc.coeFn_le, Lp.simpleFunc.toLp_eq_toLp]
case h
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
a : α
ha0 : ↑↑↑0 a = OfNat.ofNat 0 a
ha_toLp :
  ↑↑(Memℒp.toLp ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n)
            (_ : Memℒp (↑(x n)) p))
      a =
    ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n) a
⊢ ↑↑↑0 a ≤
    ↑↑(Memℒp.toLp ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n)
            (_ : Memℒp (↑(x n)) p))
      a
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
⊢ ↑↑↑0 ≤ᵐ[μ] ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p))
filter_upwards [Lp.simpleFunc.coeFn_zero p μ G, h_toLp n] with a ha0 ha_toLp
case h
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
a : α
ha0 : ↑↑↑0 a = OfNat.ofNat 0 a
ha_toLp :
  ↑↑(Memℒp.toLp ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n)
            (_ : Memℒp (↑(x n)) p))
      a =
    ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n) a
⊢ OfNat.ofNat 0 a ≤ ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n) a
case h
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
a : α
ha0 : ↑↑↑0 a = OfNat.ofNat 0 a
ha_toLp :
  ↑↑(Memℒp.toLp ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n)
            (_ : Memℒp (↑(x n)) p))
      a =
    ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n) a
⊢ ↑↑↑0 a ≤
    ↑↑(Memℒp.toLp ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n)
            (_ : Memℒp (↑(x n)) p))
      a
rw [ha0, ha_toLp]
no goals
case h
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
n : ℕ
a : α
ha0 : ↑↑↑0 a = OfNat.ofNat 0 a
ha_toLp :
  ↑↑(Memℒp.toLp ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n)
            (_ : Memℒp (↑(x n)) p))
      a =
    ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n) a
⊢ OfNat.ofNat 0 a ≤ ↑(SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n) a
exact hx_nonneg n a
case hμ
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ ∀ᵐ (x : α) ∂μ, ↑↑↑g x ∈ closure ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})

case hi
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ snorm (fun x => ↑↑↑g x - 0) p μ < ⊤
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
apply SimpleFunc.tendsto_approxOn_Lp_snorm g_meas zero_mem hp_ne_top
case hμ
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hg_nonneg : 0 ≤ᵐ[μ] ↑↑↑g
⊢ ∀ᵐ (x : α) ∂μ, ↑↑↑g x ∈ closure ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
case hμ
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ ∀ᵐ (x : α) ∂μ, ↑↑↑g x ∈ closure ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
have hg_nonneg : (0 : α → G) ≤ᵐ[μ] g := (Lp.coeFn_nonneg _).mpr g.2
case hμ
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hg_nonneg : 0 ≤ᵐ[μ] ↑↑↑g
a : α
ha : OfNat.ofNat 0 a ≤ ↑↑↑g a
⊢ ↑↑↑g a ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
case hμ
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hg_nonneg : 0 ≤ᵐ[μ] ↑↑↑g
⊢ ∀ᵐ (x : α) ∂μ, ↑↑↑g x ∈ closure ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
refine' hg_nonneg.mono fun a ha => subset_closure _
no goals
case hμ
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hg_nonneg : 0 ≤ᵐ[μ] ↑↑↑g
a : α
ha : OfNat.ofNat 0 a ≤ ↑↑↑g a
⊢ ↑↑↑g a ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
simpa using ha
case hi
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ snorm (fun x => ↑↑↑g x) p μ < ⊤
case hi
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ snorm (fun x => ↑↑↑g x - 0) p μ < ⊤
simp_rw [sub_zero]
no goals
case hi
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
⊢ snorm (fun x => ↑↑↑g x) p μ < ⊤
exact hg_memℒp.snorm_lt_top
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b => dist ↑(toLp (x b) (_ : Memℒp (↑(x b)) p)) ↑g) atTop (𝓝 0)
⊢ Tendsto
    (fun b =>
      dist
        (coeSimpleFuncNonnegToLpNonneg p μ G
          { val := toLp (x b) (_ : Memℒp (↑(x b)) p), property := (_ : 0 ≤ toLp (x b) (_ : Memℒp (↑(x b)) p)) })
        g)
    atTop (𝓝 0)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun n => ↑(toLp (x n) (_ : Memℒp (↑(x n)) p))) atTop (𝓝 ↑g)
⊢ Tendsto
    (fun n =>
      coeSimpleFuncNonnegToLpNonneg p μ G
        { val := toLp (x n) (_ : Memℒp (↑(x n)) p), property := (_ : 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)) })
    atTop (𝓝 g)
rw [tendsto_iff_dist_tendsto_zero] at this ⊢
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b => dist ↑(toLp (x b) (_ : Memℒp (↑(x b)) p)) ↑g) atTop (𝓝 0)
⊢ Tendsto
    (fun b =>
      dist
        ↑(coeSimpleFuncNonnegToLpNonneg p μ G
            {
              val :=
                toLp (SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem b)
                  (_ : Memℒp (↑(x b)) p),
              property := (_ : 0 ≤ toLp (x b) (_ : Memℒp (↑(x b)) p)) })
        ↑g)
    atTop (𝓝 0)
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b => dist ↑(toLp (x b) (_ : Memℒp (↑(x b)) p)) ↑g) atTop (𝓝 0)
⊢ Tendsto
    (fun b =>
      dist
        (coeSimpleFuncNonnegToLpNonneg p μ G
          { val := toLp (x b) (_ : Memℒp (↑(x b)) p), property := (_ : 0 ≤ toLp (x b) (_ : Memℒp (↑(x b)) p)) })
        g)
    atTop (𝓝 0)
simp_rw [Subtype.dist_eq]
no goals
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b => dist ↑(toLp (x b) (_ : Memℒp (↑(x b)) p)) ↑g) atTop (𝓝 0)
⊢ Tendsto
    (fun b =>
      dist
        ↑(coeSimpleFuncNonnegToLpNonneg p μ G
            {
              val :=
                toLp (SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem b)
                  (_ : Memℒp (↑(x b)) p),
              property := (_ : 0 ≤ toLp (x b) (_ : Memℒp (↑(x b)) p)) })
        ↑g)
    atTop (𝓝 0)
exact this
case refine_1
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x_1 => ↑↑↑(toLp (x n) (_ : Memℒp (↑(x n)) p)) x_1) =ᵐ[μ] fun x_1 => ↑(x n) x_1
case refine_1
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x_1 => ↑(x n) x_1) =ᵐ[μ] fun x_1 => ↑↑↑(toLp (x n) (_ : Memℒp (↑(x n)) p)) x_1
symm
case refine_1
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x_1 => ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) x_1) =ᵐ[μ] fun x_1 => ↑(x n) x_1
case refine_1
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x_1 => ↑↑↑(toLp (x n) (_ : Memℒp (↑(x n)) p)) x_1) =ᵐ[μ] fun x_1 => ↑(x n) x_1
rw [Lp.simpleFunc.toLp_eq_toLp]
no goals
case refine_1
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x_1 => ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) x_1) =ᵐ[μ] fun x_1 => ↑(x n) x_1
exact h_toLp n
no goals
case refine_2
α : Type u_1
β : Type ?u.2627913
ι : Type ?u.2627916
E : Type ?u.2627919
F : Type ?u.2627922
𝕜 : Type ?u.2627925
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
g : { g // 0 ≤ g }
hg_memℒp : Memℒp (↑↑↑g) p
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p
h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) (_ : Memℒp (↑(x n)) p)) =ᵐ[μ] ↑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) (_ : Memℒp (↑(x n)) p)
hx_tendsto : Tendsto (fun n => snorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ (fun x => ↑↑↑g x) =ᵐ[μ] fun x => ↑↑↑g x
rfl