α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x‖ ≤ c
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖↑(approxBounded hf c n) x‖ ≤ c
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖) • ↑(StronglyMeasurable.approx hf n) x‖ ≤ c
refine' (norm_smul_le _ _).trans _
case pos
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ‖↑(StronglyMeasurable.approx hf n) x‖ = 0
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c

case neg
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
by_cases h0 : ‖hf.approx n x‖ = 0
case neg.inl
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c

case neg.inr
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : c ≤ ‖↑(StronglyMeasurable.approx hf n) x‖
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
case neg
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
cases' le_total ‖hf.approx n x‖ c with h h
case pos
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ‖↑(StronglyMeasurable.approx hf n) x‖ = 0
⊢ 0 ≤ c
case pos
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ‖↑(StronglyMeasurable.approx hf n) x‖ = 0
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
simp only [h0, _root_.div_zero, min_eq_right, zero_le_one, norm_zero, MulZeroClass.mul_zero]
no goals
case pos
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ‖↑(StronglyMeasurable.approx hf n) x‖ = 0
⊢ 0 ≤ c
exact hc
case neg.inl
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
⊢ ‖1‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c

α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
⊢ 1 ≤ c / ‖↑(StronglyMeasurable.approx hf n) x‖
case neg.inl
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
rw [min_eq_left _]
no goals
case neg.inl
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
⊢ ‖1‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
simpa only [norm_one, one_mul] using h
no goals
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
⊢ 1 ≤ c / ‖↑(StronglyMeasurable.approx hf n) x‖
rwa [one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))]
case neg.inr
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : c ≤ ‖↑(StronglyMeasurable.approx hf n) x‖
⊢ ‖c / ‖↑(StronglyMeasurable.approx hf n) x‖‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c

α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : c ≤ ‖↑(StronglyMeasurable.approx hf n) x‖
⊢ c / ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ 1
case neg.inr
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : c ≤ ‖↑(StronglyMeasurable.approx hf n) x‖
⊢ ‖min 1 (c / ‖↑(StronglyMeasurable.approx hf n) x‖)‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
rw [min_eq_right _]
no goals
case neg.inr
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : c ≤ ‖↑(StronglyMeasurable.approx hf n) x‖
⊢ ‖c / ‖↑(StronglyMeasurable.approx hf n) x‖‖ * ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ c
rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
  inv_mul_cancel h0, one_mul, Real.norm_of_nonneg hc]
no goals
α : Type u_2
β✝ : Type ?u.41689
γ : Type ?u.41692
ι : Type ?u.41695
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖↑(StronglyMeasurable.approx hf n) x‖ = 0
h : c ≤ ‖↑(StronglyMeasurable.approx hf n) x‖
⊢ c / ‖↑(StronglyMeasurable.approx hf n) x‖ ≤ 1
rwa [div_le_one (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))]