English
A simp version shows the same bound for all x without norm assumptions.
Русский
Утверждается аналогично в упрощённом виде.
LaTeX
$$$\\forall n, \\forall x, \\|hf.approxBounded c n x\\| ≤ c$$$
Lean4
theorem norm_approxBounded_le {β} {f : α → β} [SeminormedAddCommGroup β] [NormedSpace ℝ β] {m : MeasurableSpace α}
{c : ℝ} (hf : StronglyMeasurable[m] f) (hc : 0 ≤ c) (n : ℕ) (x : α) : ‖hf.approxBounded c n x‖ ≤ c :=
by
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]
refine (norm_smul_le _ _).trans ?_
by_cases h0 : ‖hf.approx n x‖ = 0
· simp only [h0, _root_.div_zero, min_eq_right, zero_le_one, norm_zero, mul_zero]
exact hc
rcases le_total ‖hf.approx n x‖ c with h | h
· rw [min_eq_left _]
· simpa only [norm_one, one_mul] using h
· rwa [one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))]
· rw [min_eq_right _]
·
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]
· rwa [div_le_one (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))]
