/-- The **logistic map** `f_r(x) = r x (1 - x)`, a model of a population with limited resources(`x` is the population as a fraction of its maximum, `r` the growth rate). -/def logistic (r x : ℝ) : ℝ := r * x * (1 - x)
iterate_contractiontheoremProved here from basic factspropext, Classical.choice, Quot.sound
iterate_contractionLean 4Proved here from basic factsFormally verified
/-- **The basic estimate.** If `f` fixes `a`, maps the interval `I = [a - δ, a + δ]` into itselfand pulls every point of `I` towards `a` by a factor `K` (`|f x - a| ≤ K |x - a|`), then`|fⁿ(x) - a| ≤ Kⁿ |x - a|` for `x ∈ I`. Induction on `n`. -/theorem iterate_contraction {f : ℝ → ℝ} {a δ K : ℝ} (hK0 : 0 ≤ K) (hK1 : K ≤ 1) (hpull : ∀ x ∈ Icc (a - δ) (a + δ), |f x - a| ≤ K * |x - a|) : ∀ n : ℕ, ∀ x ∈ Icc (a - δ) (a + δ), f^[n] x ∈ Icc (a - δ) (a + δ) ∧ |f^[n] x - a| ≤ K ^ n * |x - a| := by have hmem : ∀ x, x ∈ Icc (a - δ) (a + δ) ↔ |x - a| ≤ δ := fun x => by rw [abs_le, mem_Icc]; constructor <;> rintro ⟨h1, h2⟩ <;> constructor <;> linarith intro n induction n with | zero => intro x hx; simp [hx] | succ n ih => intro x hx obtain ⟨hin, hbound⟩ := ih x hx rw [iterate_succ_apply'] have step := hpull _ hin have hδ : |f^[n] x - a| ≤ δ := (hmem _).mp hin refine ⟨(hmem _).mpr ?_, ?_⟩ · calc |f (f^[n] x) - a| ≤ K * |f^[n] x - a| := step _ ≤ 1 * δ := mul_le_mul hK1 hδ (abs_nonneg _) zero_le_one _ = δ := one_mul δ · calc |f (f^[n] x) - a| ≤ K * |f^[n] x - a| := step _ ≤ K * (K ^ n * |x - a|) := mul_le_mul_of_nonneg_left hbound hK0 _ = K ^ (n + 1) * |x - a| := by ring
attracting_fixed_pointtheoremProved here from basic factspropext, Classical.choice, Quot.sound
attracting_fixed_pointLean 4Proved here from basic factsFormally verified
/-- **Attracting fixed point theorem.** Let `f(a) = a`, and suppose `f` is differentiable on`I = [a - δ, a + δ]` with `|f'| ≤ K < 1` there. Then every orbit starting in `I` converges to `a`.Proof: the mean value inequality gives `|f x - a| = |f x - f a| ≤ K |x - a|` on `I`; then`iterate_contraction` gives `|fⁿ(x) - a| ≤ Kⁿ |x - a| → 0`. (If `f` is C¹ with `|f'(a)| < 1`,continuity of `f'` provides such a `δ` and `K`.) -/theorem attracting_fixed_point {f : ℝ → ℝ} {a δ K : ℝ} (hfix : f a = a) (hδ : 0 ≤ δ) (hK0 : 0 ≤ K) (hK1 : K < 1) (hdiff : ∀ x ∈ Icc (a - δ) (a + δ), DifferentiableAt ℝ f x) (hderiv : ∀ x ∈ Icc (a - δ) (a + δ), |deriv f x| ≤ K) {x : ℝ} (hx : x ∈ Icc (a - δ) (a + δ)) : Tendsto (fun n => f^[n] x) atTop (𝓝 a) := by have ha : a ∈ Icc (a - δ) (a + δ) := ⟨by linarith, by linarith⟩ have hpull : ∀ y ∈ Icc (a - δ) (a + δ), |f y - a| ≤ K * |y - a| := by intro y hy have := (convex_Icc (a - δ) (a + δ)).norm_image_sub_le_of_norm_deriv_le hdiff (fun z hz => by rw [Real.norm_eq_abs]; exact hderiv z hz) ha hy simpa [Real.norm_eq_abs, hfix] using this have hbound := iterate_contraction hK0 hK1.le hpull -- `Kⁿ |x - a| → 0`, and `|fⁿ x - a|` is squeezed below it. have hlim : Tendsto (fun n : ℕ => K ^ n * |x - a|) atTop (𝓝 0) := by simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one hK0 hK1).mul_const |x - a| rw [tendsto_iff_norm_sub_tendsto_zero] refine squeeze_zero (fun n => norm_nonneg _) (fun n => ?_) hlim rw [Real.norm_eq_abs] exact (hbound n x hx).2
banach_fixed_pointtheoremApplies a library theorempropext, Classical.choice, Quot.sound
banach_fixed_pointLean 4Applies a library theoremFormally verified
/-- **Banach's fixed point theorem**: a contraction of a non-empty complete metric space has aunique fixed point, and every orbit converges to it. This applies Mathlib's`ContractingWith.tendsto_iterate_fixedPoint` (and `ContractingWith.fixedPoint_isFixedPt`). -/theorem banach_fixed_point {X : Type*} [MetricSpace X] [CompleteSpace X] [Nonempty X] {K : NNReal} {f : X → X} (hf : ContractingWith K f) (x : X) : IsFixedPt f (ContractingWith.fixedPoint f hf) ∧ Tendsto (fun n => f^[n] x) atTop (𝓝 (ContractingWith.fixedPoint f hf)) := ⟨ContractingWith.fixedPoint_isFixedPt hf, hf.tendsto_iterate_fixedPoint x⟩
doubling_separatestheoremProved here from basic factspropext, Classical.choice, Quot.sound
doubling_separatesLean 4Proved here from basic factsFormally verified
/-- **Nearby orbits of the doubling map separate exponentially.** For the lift `D(x) = 2x` of thedoubling map `x ↦ 2x mod 1`, two orbits starting at distance `d` are at distance `2ⁿ d` after `n`steps. So an initial uncertainty of `10⁻¹⁰` grows to order `1` within about 33 steps: theLyapunov exponent is `ln 2`. -/theorem doubling_separates (x y : ℝ) (n : ℕ) : (fun z : ℝ => 2 * z)^[n] x - (fun z : ℝ => 2 * z)^[n] y = 2 ^ n * (x - y) := by induction n with | zero => simp | succ n ih => rw [iterate_succ_apply', iterate_succ_apply', ← mul_sub, ih] ring
lyapunov_decaytheoremProved here from basic factspropext, Classical.choice, Quot.sound
lyapunov_decayLean 4Proved here from basic factsFormally verified
/-- **A Lyapunov function for the spiral sink** `x' = -x + y`, `y' = -x - y`. Along any solution,`V = x² + y²` satisfies `V' = 2x(-x + y) + 2y(-x - y) = -2V`, so `V(t) = V(0) e^{-2t}`: everysolution spirals into the origin. Proof: `V(t) e^{2t}` has derivative `0`, hence is constant. -/theorem lyapunov_decay {x y : ℝ → ℝ} (hx : ∀ t, HasDerivAt x (-x t + y t) t) (hy : ∀ t, HasDerivAt y (-x t - y t) t) (t : ℝ) : x t ^ 2 + y t ^ 2 = (x 0 ^ 2 + y 0 ^ 2) * Real.exp (-2 * t) := by set W : ℝ → ℝ := fun s => (x s ^ 2 + y s ^ 2) * Real.exp (2 * s) with hW have hWd : ∀ s, HasDerivAt W 0 s := by intro s have h1 := (((hx s).pow 2).add ((hy s).pow 2)).mul (((hasDerivAt_id' s).const_mul 2).exp) convert h1 using 1 simp only [Pi.add_apply, Pi.pow_apply, Nat.cast_ofNat] ring have hconst : W t = W 0 := is_const_of_deriv_eq_zero (fun s => (hWd s).differentiableAt) (fun s => (hWd s).deriv) t 0 have hexp : Real.exp (2 * t) * Real.exp (-2 * t) = 1 := by rw [← Real.exp_add]; simp simp only [hW, mul_zero, Real.exp_zero, mul_one] at hconst calc x t ^ 2 + y t ^ 2 = (x t ^ 2 + y t ^ 2) * (Real.exp (2 * t) * Real.exp (-2 * t)) := by rw [hexp, mul_one] _ = ((x t ^ 2 + y t ^ 2) * Real.exp (2 * t)) * Real.exp (-2 * t) := by ring _ = (x 0 ^ 2 + y 0 ^ 2) * Real.exp (-2 * t) := by rw [hconst]
/-- The multiplier of the fixed point `1 - 1/r` of the logistic map is `2 - r`. Show that it hasabsolute value less than `1` exactly when `1 < r < 3`.Hint: `rw [abs_lt]`, then split both directions and finish with `linarith`. -/theorem logistic_stable_iff (r : ℝ) : |2 - r| < 1 ↔ 1 < r ∧ r < 3 := by sorry
Show the compiled solution
logistic_stable_iffLean 4Proved here from basic factsFormally verified
/-- **When is `1 - 1/r` attracting?** Its multiplier `2 - r` satisfies `|2 - r| < 1` exactly when`1 < r < 3`. (At `r = 3` the multiplier passes through `-1`: a period-doubling bifurcation.) -/theorem logistic_stable_iff (r : ℝ) : |2 - r| < 1 ↔ 1 < r ∧ r < 3 := by rw [abs_lt] constructor · rintro ⟨h1, h2⟩; constructor <;> linarith · rintro ⟨h1, h2⟩; constructor <;> linarith
/-- Show that `n` steps of `z ↦ 2z` multiply the distance between two points by `2ⁿ`.Hint: induction on `n`; `Function.iterate_succ_apply'` rewrites `f^[n+1] x` as `f (f^[n] x)`. -/theorem doubling_separates (x y : ℝ) (n : ℕ) : (fun z : ℝ => 2 * z)^[n] x - (fun z : ℝ => 2 * z)^[n] y = 2 ^ n * (x - y) := by sorry
Show the compiled solution
doubling_separatesLean 4Proved here from basic factsFormally verified
/-- **Nearby orbits of the doubling map separate exponentially.** For the lift `D(x) = 2x` of thedoubling map `x ↦ 2x mod 1`, two orbits starting at distance `d` are at distance `2ⁿ d` after `n`steps. So an initial uncertainty of `10⁻¹⁰` grows to order `1` within about 33 steps: theLyapunov exponent is `ln 2`. -/theorem doubling_separates (x y : ℝ) (n : ℕ) : (fun z : ℝ => 2 * z)^[n] x - (fun z : ℝ => 2 * z)^[n] y = 2 ^ n * (x - y) := by induction n with | zero => simp | succ n ih => rw [iterate_succ_apply', iterate_succ_apply', ← mul_sub, ih] ring