α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => ↑(approxBounded hf c n) x) atTop (𝓝 (f x))
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
⊢ Tendsto (fun n => ↑(approxBounded hf c n) x) atTop (𝓝 (f x))
have h_tendsto := hf.tendsto_approx x
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => ↑(approxBounded hf c n) x) atTop (𝓝 (f x))
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))

case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))
by_cases hfx0 : ‖f x‖ = 0
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (1 • f x))
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))
rw [← one_smul ℝ (f x)]
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)) atTop (𝓝 1)
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (1 • f x))
refine' Tendsto.smul _ h_tendsto
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)) atTop (𝓝 1)
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)) atTop (𝓝 1)
have : min 1 (c / ‖f x‖) = 1 := by
  rw [min_eq_left_iff, one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfx0))]
  exact hfx
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)) atTop (𝓝 (min 1 (c / ‖f x‖)))
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)) atTop (𝓝 1)
nth_rw 2 [this.symm]
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun n => c / ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 (c / ‖f x‖))
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)) atTop (𝓝 (min 1 (c / ‖f x‖)))
refine' Tendsto.min tendsto_const_nhds _
no goals
case neg
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun n => c / ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 (c / ‖f x‖))
refine' Tendsto.div tendsto_const_nhds h_tendsto.norm hfx0
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : f x = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))
rw [norm_eq_zero] at hfx0
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : f x = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop
    (𝓝 (f x))
rw [hfx0] at h_tendsto ⊢
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
have h_tendsto_norm : Tendsto (fun n => ‖hf.approx n x‖) atTop (𝓝 0) := by
  convert h_tendsto.norm
  rw [norm_zero]
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x‖ ≤
    ‖↑(StronglyMeasurable.approx hf n) x‖
case pos
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
⊢ Tendsto (fun n => min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
refine' squeeze_zero_norm (fun n => _) h_tendsto_norm
case h.e'_5.h.e'_3
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ 0 = ‖0‖
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
convert h_tendsto.norm
no goals
case h.e'_5.h.e'_3
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ 0 = ‖0‖
rw [norm_zero]
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ ≤ ‖1‖
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤
    ‖1‖ * ‖↑(StronglyMeasurable.approx hf n) x‖
refine' mul_le_mul_of_nonneg_right _ (norm_nonneg _)
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) ≤ 1

α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ 0 ≤ min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ ≤ ‖1‖
rw [norm_one, Real.norm_of_nonneg]
no goals
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) ≤ 1
exact min_le_left _ _
no goals
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ 0 ≤ min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)
exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))
no goals
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖↑(StronglyMeasurable.approx hf n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖1‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ = ‖↑(StronglyMeasurable.approx hf n) x‖
rw [norm_one, one_mul]
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ ‖f x‖ ≤ c
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ min 1 (c / ‖f x‖) = 1
rw [min_eq_left_iff, one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfx0))]
no goals
α : Type u_2
β✝ : Type ?u.23759
γ : Type ?u.23762
ι : Type ?u.23765
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ ‖f x‖ ≤ c
exact hfx