Shrinking epsilon in analysis proofs

Stream: mathlib4

[Winston Yin (尹維晨)]

I'd like to suggest, if it doesn't already exist, an API/tactic for writing analysis proofs.

A standard proof procedure in real analysis is show ∃ ε > 0, P ε. So you first obtain some ε and hε : 0 < ε from, say, an open ball inside a neighbourhood set, and you do refine ⟨ε, hε, ?_⟩, hoping that P ε follows.

Halfway through the proof of P ε, you realise you actually needed ε / 2, or maybe min ε ε', where ε' > 0 has to be obtained from, say, the continuity of some function. In informal mathematics, you just say "shrink ε to ε / 2" or "let εmin be the smallest out of ε1, ε2, ε3". The statements P1 ε1, P2 ε2, P3 ε3 that held before are presumed to still hold for εmin.

In Lean, you have to go back and rewrite refine ⟨min ε ε', ?_, ?_⟩, and then you need all these code blocks that show that the statements that held for ε now still hold for ε / 2 or εmin. Every time such shrinkage of ε happens, you need to tediously modify all the previous code by adding a bunch of half_pos or min_le_[left|right]. I'm hoping that Lean has a better way to handle this sort of proofs.

You may argue that any good proof formaliser should first write the proof down nicely on paper, figure out that the correct ε you need is εmin = min (ε1 / 2) (min (ε2 / 4) (min ε3 ε4)), and then get it right in Lean the first time. One, this still invovles a lot of tedious nesting of min_le_[left|right] that clutter the overall argument. Two, you still need to show that if Pi εmin holds for every i; more clutter. Three, this doesn't correspond to how one actually thinks through a proof in real analysis, even when one already knows the proof by heart.

I faced this problem in #8886, where I needed to get εmin as the min of SIX different εs extracted from various conditions. I experimented with the following design, which you can see in action in IntegralCurve.lean. I introduced a Prop called Shrinkable (for lack of a better name), which takes in p : ℝ → Prop. Shrinkable p basically says that if p ε holds, then p ε' also holds for a smaller ε'.

In the actual proof, you first show that h1 : p1 ε1 holds for some ε1. Later on you have another ε2 for which h2 : p2 ε2 holds. You then show that hp1 : Shrinkable p1 and hp2 : Shrinkable p2, which are lemmas tucked elsewhere (can instance synthesis help?). Now, hp1 h1 (min_le_left ε1 ε2) : p1 (min ε1 ε2) can be directly used in the grand finale, after refine ⟨min ε1 ε2, ?_, ?_⟩ is invoked.

I hope what I'm describing is clear! What do you think?

[Mario Carneiro]

I think the clean way to do this kind of proof is using the filter_upwards tactic

[Winston Yin (尹維晨)]

Oh so an easy way already exists?

[Winston Yin (尹維晨)]

Let me read into it and not reinvent the wheel!

[Mario Carneiro]

it will handle min reasoning but not / 2 reasoning

[Mario Carneiro]

although I suppose you can do / 2 reasoning using the uniformity filter

[Patrick Massot]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Assigning.20metavariables.20by.20unification/near/407350443

[Winston Yin (尹維晨)]

It's not immediately clear to me how to use filter_upwards for the proof in #8886 in a clean way :neutral:

[Patrick Massot]

Could you tell me where precisely you have this issue?

[Winston Yin (尹維晨)]

I'll think a little harder first :)

[Winston Yin (尹維晨)]

I'm guessing the idiomatic way with filter_upwards is not to reason with ε so soon

[Winston Yin (尹維晨)]

Reason with sets in the neighbourhood filter first

[Patrick Massot]

The way filters are meant to handle this is as follows.

have F₁ : ∀ᶠ ε in 𝓝 (0 : ℝ), P₁ ε := sorry
have F₂ : ∀ᶠ ε in 𝓝 (0 : ℝ), P₂ ε := sorry
have F₃ : ∀ᶠ ε in 𝓝 (0 : ℝ), P₃ ε := sorry
have : ∀ᶠ ε in 𝓝 (0 : ℝ), P₁ ε ∧ P₂ ε ∧ P₃ ε := F₁.and (F₂.and F₃)

[Patrick Massot]

And you can use docs#Metric.eventually_nhds_iff_ball to get out of filter world.

[Patrick Massot]

There is probably an even more specialized version for real numbers.

[Patrick Massot]

You can at least do something like simp [Metric.eventually_nhds_iff_ball, Real.dist_0_eq_abs] at this to turn this into ∃ ε, 0 < ε ∧ ∀ t : ℝ, |t| < ε → P₁ t ∧ P₂ t ∧ P₃ t.

[Winston Yin (尹維晨)]

Very helpful. Thank you!

[Patrick Massot]

And really ∀ᶠ ε in 𝓝 (0 : ℝ), P₁ ε reads as "for every ε close to 0, P₁ ε".

[Junyan Xu]

The appropriate filter might be nhdsWithin 0 (Set.Ioi 0) which for example appears in this file.

[Patrick Massot]

Also known as the much friendlier looking 𝓝[>] 0.

[Junyan Xu]

Yeah the notation is used in the code but I don't know where it's introduced ...

[Patrick Massot]

https://github.com/leanprover-community/mathlib4/blob/5973b7110e5745124d413dd9b88c6118668adf4e//Mathlib/Topology/Basic.lean#L845-L863

[Winston Yin (尹維晨)]

It's great to know this standard way using filters. Does Mathematics in Lean have examples of a translation of standard epsilon-delta proofs using filters?

[Patrick Massot]

Section 9.1 contains quite a bit about that.

[Patrick Massot]

I don't remember the exact details because I wrote that more than one year ago.

[Patrick Massot]

https://leanprover-community.github.io/mathematics_in_lean/C09_Topology.html

[Patrick Massot]

You should start with the introduction to Chapter 9, even before 9.1

[Winston Yin (尹維晨)]

I think I'm understanding how Eventually works now. Thank you all!

[Winston Yin (尹維晨)]

Filters are maybe not quite as intuitive, but I managed to refactor #8886 using filters. Filter.Eventually.and really helped me extract a clean, smallest, neighbourhood at the end. No more mins or going back to rewrite previous code!

[Patrick Massot]

Don't worry, you will soon find filters much more intuitive than epsilon-wrangling, starting here.