The excised parameter set shrinks to nothing

An ε-excision deletes from the parameter interval every time at which the curve comes within ε of one of finitely many centres. This file records that the deleted set carries no length in the limit: the integral of the excision's indicator over [a, b] tends to b - a as ε → 0⁺.

Two properties of the curve are used, for two different parts of the argument. Measurability makes each excised set measurable. Nullity of the times the curve spends exactly at a centre gives the almost-everywhere convergence: away from those times the curve keeps a positive distance from the finite centre set, so the excision condition eventually fails outright. Injectivity on [a, b] is one convenient sufficient condition for the second — it makes those times finite — and is recorded separately as measure_setOf_mem_eq_zero_of_injOn; a curve may revisit centres, so long as it does so on a null set of times.

Main results

• TauCeti.Contour.nullMeasurableSet_excision: the excised parameter set is null-measurable against any measure for which the curve is a.e. measurable.
• TauCeti.Contour.measurableSet_excision: its measurable specialization.
• TauCeti.Contour.measure_setOf_mem_eq_zero_of_injOn: an injective curve meets a finite set at a null set of times.
• TauCeti.Contour.tendsto_intervalIntegral_excisionIndicator: the excision indicator's integral over [a, b] tends to b - a as ε → 0⁺.

References

• AINTLIB LeanModularForms — the valence-formula development. This file adapts the measure-theoretic step of ForMathlib/ValenceFormula/PVChain/ArcContribution.lean (arc_non_excluded_measure_tendsto, with its arc_preimage_subsingleton and arc_min_dist_pos helpers) onto the current Mathlib pin, restated for an arbitrary curve rather than the fundamental-domain arc.

theorem TauCeti.Contour.nullMeasurableSet_excision {γ : ℝ → ℂ} {μ : MeasureTheory.Measure ℝ} (hγ : AEMeasurable γ μ) (S : Finset ℂ) (ε : ℝ) : MeasureTheory.NullMeasurableSet {t : ℝ | ∃ s ∈ S, ‖γ t - s‖ ≤ ε} μ

The excised parameter set is null-measurable. The finite union, over the centres, of the sublevel sets of t ↦ ‖γ t - s‖, each null-measurable because γ is a.e. measurable. Stated for an arbitrary measure so that it serves both the ambient statement and the restricted-measure one that interval integrability needs.

theorem TauCeti.Contour.measurableSet_excision {γ : ℝ → ℂ} (hγm : Measurable γ) (S : Finset ℂ) (ε : ℝ) : MeasurableSet {t : ℝ | ∃ s ∈ S, ‖γ t - s‖ ≤ ε}

The excised parameter set is measurable. It is the finite union, over the centres, of the preimages of the ray (-∞, ε] under t ↦ ‖γ t - s‖, each measurable because γ is.

theorem TauCeti.Contour.measure_setOf_mem_eq_zero_of_injOn {γ : ℝ → ℂ} {a b : ℝ} (hγ : Set.InjOn γ (Set.Icc a b)) (S : Finset ℂ) : MeasureTheory.volume {t : ℝ | t ∈ Set.Icc a b ∧ γ t ∈ S} = 0

An injective curve meets a finite set at a null set of times. It meets it at finitely many times — at most one per centre — so those times carry no length. This is the convenient sufficient condition for tendsto_intervalIntegral_excisionIndicator's hypothesis.

theorem TauCeti.Contour.tendsto_intervalIntegral_excisionIndicator {γ : ℝ → ℂ} (hγm : Measurable γ) {a b : ℝ} (hab : a ≤ b) (S : Finset ℂ) (hnull : MeasureTheory.volume {t : ℝ | t ∈ Set.Icc a b ∧ γ t ∈ S} = 0) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else 1) (nhdsWithin 0 (Set.Ioi 0)) (nhds (b - a))

The excised parameter set shrinks to nothing. Deleting from [a, b] the times at which the curve comes within ε of one of finitely many centres costs no length as ε → 0⁺: what survives tends to the whole length b - a.

The curve must be measurable, and must spend only a null set of times exactly at a centre — measure_setOf_mem_eq_zero_of_injOn supplies the latter from injectivity.