English
If 1 < ||c||, then egauge on ball of radius r is bounded by a multiple of ||c|| and ||x|| divided by r, provided nondegeneracy holds.
Русский
Если 1 < ||c||, то egauge шар радиуса r ограничен константой, пропорциональной ||c|| и ||x||/r, при условии ненулевых значений.
LaTeX
$$$\\forall c, x, r:\\; 1 < \\|c\\| \\Rightarrow (r ≠ 0 \\lor \\|x\\| ≠ 0) \\Rightarrow egauge 𝕜 (ball 0 r) x \\le \\frac{\\|c\\|_e \\cdot \\|x\\|_e}{r}.$$$
Lean4
theorem egauge_ball_le_of_one_lt_norm (hc : 1 < ‖c‖) (h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0) : egauge 𝕜 (ball 0 r) x ≤ ‖c‖ₑ * ‖x‖ₑ / r :=
by
letI : NontriviallyNormedField 𝕜 := ⟨c, hc⟩
rcases (zero_le r).eq_or_lt with rfl | hr
· rw [ENNReal.coe_zero, ENNReal.div_zero (mul_ne_zero _ _)]
· apply le_top
· simpa using one_pos.trans hc
· simpa [enorm, ← NNReal.coe_eq_zero] using h₀
· rcases eq_or_ne ‖x‖ 0 with hx | hx
· have hx' : ‖x‖ₑ = 0 := by simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx
simp only [hx', mul_zero, ENNReal.zero_div, nonpos_iff_eq_zero, egauge_eq_zero_iff]
refine (frequently_iff_neBot.2 (inferInstance : NeBot (𝓝[≠] (0 : 𝕜)))).mono fun c hc ↦ ?_
simp [mem_smul_set_iff_inv_smul_mem₀ hc, norm_smul, hx, hr]
· rcases rescale_to_shell_semi_normed hc hr hx with ⟨a, ha₀, har, -, hainv⟩
calc
egauge 𝕜 (ball 0 r) x ≤ ↑(‖a‖₊⁻¹) := egauge_le_of_smul_mem_of_ne (mem_ball_zero_iff.2 har) ha₀
_ ≤ ↑(‖c‖₊ * ‖x‖₊ / r) := by rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
_ ≤ ‖c‖ₑ * ‖x‖ₑ / r := ENNReal.coe_div_le.trans <| by simp [ENNReal.coe_mul, enorm]
