English
Same submultiplicativity as in 56605: seminormFromBounded' f (xy) ≤ seminormFromBounded' f x · seminormFromBounded' f y.
Русский
Та же субумножаемость: seminormFromBounded' f (xy) ≤ seminormFromBounded' f x · seminormFromBounded' f y.
LaTeX
$$$\operatorname{seminormFromBounded}' f (x y) \le \operatorname{seminormFromBounded}' f x \cdot \operatorname{seminormFromBounded}' f y$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f` is submultiplicative. -/
theorem seminormFromBounded_mul (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x y : R) :
seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y :=
by
apply ciSup_le
by_cases hy : seminormFromBounded' f y = 0
· rw [seminormFromBounded_eq_zero_iff f_nonneg f_mul] at hy
intro z
rw [mul_comm x y, mul_assoc, map_mul_zero_of_map_zero f_nonneg f_mul hy (x * z), zero_div]
exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul x) (seminormFromBounded_nonneg f_nonneg f_mul y)
· intro z
rw [← div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy)]
apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z
rw [div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy), div_mul_eq_mul_div]
by_cases hz : f z = 0
· have hxyz : f (z * (x * y)) = 0 := map_mul_zero_of_map_zero f_nonneg f_mul hz _
simp_rw [mul_comm, hxyz, zero_div]
exact div_nonneg (mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _)) (f_nonneg _)
· rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), mul_comm (f (x * z))]
by_cases hxz : f (x * z) = 0
· rw [mul_comm x y, mul_assoc, mul_comm y, map_mul_zero_of_map_zero f_nonneg f_mul hxz y]
exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _)
· rw [← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hxz)]
apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) (x * z)
rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hxz), mul_comm x y, mul_assoc]
