discontinuity of a step function

Stream: maths

[Joseph Corneli]

My step function:

noncomputable def step_fun : ℝ → ℝ := λ x, if x ≤ ξ then 1 else 0

Relevant lemmas: continuous_iff_continuous_at and tendsto_nhds_nhds. Using these I can change from the neighbourhoods/filters language into more typical epsilon/delta langauge. The lemmas are if-and-only-if results, so useful for deriving the negative (discontinuity) result that I'm aiming for.

Now, clearly you can choose points as close to ξ (from the right) as you wish, and their values will always be distance 1 away from f ξ, which is 1.

For example, setting ε to 1/2, there is no such δ>0 with the property that ∀ {x : ℝ}, dist x ξ < δ → dist (step_fun x) (step_fun ξ) < ε). But how to get this fact across to Lean?

import data.real.basic data.complex.exponential topology.basic data.set.intervals analysis.exponential order.filter.basic

constants (ξ : ℝ)
open real

noncomputable def step_fun : ℝ → ℝ := λ x, if x ≤ ξ then 1 else 0

lemma discont_at_step : ¬ (continuous_at step_fun ξ) := begin
unfold continuous_at,
-- our goal:
-- ⊢ ¬filter.tendsto step_fun (nhds ξ) (nhds (step_fun ξ))
rw metric.tendsto_nhds_nhds,
-- our goal:
-- ⊢ ¬∀ (ε : ℝ),
--      ε > 0 → (∃ (δ : ℝ) (H : δ > 0),
--                ∀ {x : ℝ}, dist x ξ < δ → dist (step_fun x)
--                                               (step_fun ξ) < ε)
end

[Chris Hughes]

You might need more recent mathlib for this, but Patrick's push_neg tactic will help. Try import tactic.push_neg

[Chris Hughes]

Note the use of push_neg

lemma discont_at_step : ¬ (continuous_at step_fun ξ) :=
begin
  unfold continuous_at,
  -- our goal:
  -- ⊢ ¬filter.tendsto step_fun (nhds ξ) (nhds (step_fun ξ))
  rw metric.tendsto_nhds_nhds,
  push_neg,
  -- goal
  -- ∃ (ε : ℝ), ε > 0 ∧ ∀ (δ : ℝ), δ > 0 → (∃ {x : ℝ},
  -- dist x ξ < δ ∧ ε ≤ dist (step_fun x) (step_fun ξ))
  use 1/2,
  refine ⟨by norm_num, _⟩,
  assume δ δ0,
  use ξ + δ / 2,
  split,
  { simp [real.dist_eq, abs_of_nonneg (le_of_lt (half_pos δ0)), half_lt_self δ0] },
  { have : ¬ ξ + δ / 2 ≤ ξ, from not_le_of_gt ((lt_add_iff_pos_right _).2 (half_pos δ0)),
    simp [real.dist_eq, step_fun, le_refl, this],
    norm_num }
end

[Joseph Corneli]

Thanks Chris! I saw push_neg mentioned in the commits. I'll have to spend some time grokking the rest of the proof but it looks quite comprehensible. Cheers.

[Patrick Massot]

Chris is showing you the noble art of knowing all elementary inequality lemmas of mathlib, but there dark side is much quicker, you can replace the end of the proof by:

  { rw [real.dist_eq, abs_of_nonneg] ; linarith },
  { have I1 : ¬ ξ + δ / 2 ≤ ξ, by linarith,
    have I2 : ξ ≤ ξ, by linarith,
    have I3 : (2: ℝ)⁻¹ ≤ 1, by norm_num,
    simp [real.dist_eq, step_fun, I1, I2, I3] }

The second half is a bit disappointing, I guess one could have find a better tactic here. Scott?

[Patrick Massot]

Also, Joe, what is the point of having xi declared as a constant?