function restricted to n < bound has finite image

Stream: Is there code for X?

[Kevin Buzzard]

This came up in code review:

import Mathlib

/-- The function which is `f` up to `bound` and then `0` afterwards. -/
def truncation (f : ℕ → ℝ) (bound : ℕ) : ℕ → ℝ := fun n ↦
  if n < bound then f n else 0

theorem truncation_bddAbove (f : ℕ → ℝ) (bound : ℕ) :
    BddAbove (Set.range (truncation f bound)) :=
  sorry

theorem truncation_finite_range (f : ℕ → ℝ) (bound : ℕ) :
    (Set.range (truncation f bound)).Finite :=
  sorry

Presumably there are very short proofs of these? I don't know the tricks though :-(

[Yaël Dillies]

import Mathlib

/-- The function which is `f` up to `bound` and then `0` afterwards. -/
def truncation (f : ℕ → ℝ) (bound : ℕ) : ℕ → ℝ := fun n ↦
  if n < bound then f n else 0

theorem truncation_finite_range (f : ℕ → ℝ) (bound : ℕ) :
    (Set.range (truncation f bound)).Finite :=
  .subset (.union (Set.finite_singleton 0) <| (Set.finite_Iio bound).image f) <| by
    aesop (add simp [Set.range_subset_iff, truncation])

theorem truncation_bddAbove (f : ℕ → ℝ) (bound : ℕ) :
    BddAbove (Set.range (truncation f bound)) :=
  (truncation_finite_range ..).bddAbove

[Yaël Dillies]

Braindead proof. I'm sure it can be golfed further

[Kevin Buzzard]

Thanks a lot! As far as I'm concerned this is short enough.

[Michael Rothgang]

Something like this should also hold for continuous functions (truncated to a bounded interval). I'm saying this because the Carleson project also uses truncations, but for functions defined on (ENN)Real.

[Michael Rothgang]

Perhaps these are sufficiently separate to not warrant worrying about a common generalisation.

[Kevin Buzzard]

Well my function is continuous and the restriction is to a compact subset...

[Michael Rothgang]

Yes, it is! But you're not proving a lemma about that, are you?