Persistence of the absence of intermediate returns

Proved

BianchiIX.eventually_no_intermediate_return

by trppppp · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

Let $X$ be a topological space, $x_0\in X$ , $T:X\to\mathbb R$ be continuous at $x_0$ with $T(x_0)>0$ , and $g:X\times\mathbb R\to\mathbb R$ . Fix $c\in\mathbb R$ . Assume that $g(x,t)=c$ implies $t=0$ near $(x_0,0)$ and implies $t=T(x)$ near $(x_0,T(x_0))$ . Suppose $g$ is continuous at every $(x_0,t)$ with $0<t<T(x_0)$ and $g(x_0,t)\ne c$ there. Then for all $x$ sufficiently near $x_0$ ,

g(x,t)\ne c\quad(0<t<T(x)).

Preamble

import Mathlib.Topology.Order.IntermediateValue
import Mathlib.Topology.Order.Compact
import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Tactic.Linarith

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set Filter
open scoped Topology
variable {X : Type*} [TopologicalSpace X]

Formal statement

theorem BianchiIX.eventually_no_intermediate_return {x₀ : X} {T : X → ℝ}
    {g : X → ℝ → ℝ} {c : ℝ} (hT : ContinuousAt T x₀) (hpos : 0 < T x₀)
    (hentry : ∀ᶠ z : X × ℝ in 𝓝 (x₀, 0), g z.1 z.2 = c → z.2 = 0)
    (hexit : ∀ᶠ z : X × ℝ in 𝓝 (x₀, T x₀), g z.1 z.2 = c → z.2 = T z.1)
    (hcont : ∀ t ∈ Ioo 0 (T x₀), ContinuousAt (fun z : X × ℝ => g z.1 z.2) (x₀, t))
    (havoid : ∀ t ∈ Ioo 0 (T x₀), g x₀ t ≠ c) :
    ∀ᶠ x in 𝓝 x₀, ∀ t ∈ Ioo 0 (T x), g x t ≠ c := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/FirstReturnPersistence.lean#L35-L59

View graph