Profiles.lean

1 import KomorebiSpace.Cofinal
2 import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
3 import Mathlib.Topology.Instances.Real.Lemmas
4 import Mathlib.Tactic.NormNum
5 import Mathlib.Tactic.Linarith
6 
7 set_option autoImplicit false
8 
9 /-!
10 # What cofinal refinement does and does not preserve
11 
12 Vanishing is invariant under monotone cofinal sampling for a nonnegative
13 nonincreasing residual profile. Without monotonicity, even cofinal sampling
14 can hide every nonzero residual. Raw residual norms are not invariants by fiat.
15 -/
16 namespace KomorebiSpace
17 namespace Profiles
18 open Filter
19 open scoped Topology
20 
21 theorem schedule_tendsto_atTop (φ : ℕ → ℕ) (hφ : Monotone φ)
22     (hc : Resolution.UnboundedSchedule φ) : Tendsto φ atTop atTop := by
23   apply tendsto_atTop.2
24   intro n
25   obtain ⟨j, hj⟩ := hc n
26   exact eventually_atTop.2 ⟨j, fun k hk => hj.trans (hφ hk)⟩
27 
28 theorem vanish_of_sample (η : ℕ → ℝ) (hη : ∀ n, 0 ≤ η n)
29     (hanti : Antitone η) (φ : ℕ → ℕ)
30     (hs : Tendsto (fun n => η (φ n)) atTop (𝓝 0)) : Tendsto η atTop (𝓝 0) := by
31   apply Metric.tendsto_atTop.2
32   intro ε hε
33   have hev : ∀ᶠ k in atTop, η (φ k) < ε := (tendsto_order.1 hs).2 ε hε
34   obtain ⟨k, hk⟩ := hev.exists
35   refine ⟨φ k, ?_⟩
36   intro n hn
37   have hlt : η n < ε := (hanti hn).trans_lt hk
38   simpa only [Real.dist_eq, sub_zero, abs_of_nonneg (hη n)] using hlt
39 
40 /-- Correct quantitative cofinal-invariance theorem: only a convergence property. -/
41 theorem cofinal_vanish_iff (η : ℕ → ℝ) (hη : ∀ n, 0 ≤ η n)
42     (hanti : Antitone η) (φ : ℕ → ℕ) (hφ : Monotone φ)
43     (hc : Resolution.UnboundedSchedule φ) :
44     Tendsto η atTop (𝓝 0) ↔ Tendsto (fun n => η (φ n)) atTop (𝓝 0) := by
45   constructor
46   · intro h
47     exact h.comp (schedule_tendsto_atTop φ hφ hc)
48   · exact vanish_of_sample η hη hanti φ
49 
50 def alternating (n : ℕ) : ℝ := if n % 2 = 0 then 0 else 1
51 
52 @[simp] theorem alternating_even (n : ℕ) : alternating (2*n) = 0 := by
53   have h : (2*n) % 2 = 0 := by omega
54   simp [alternating, h]
55 
56 @[simp] theorem alternating_odd (n : ℕ) : alternating (2*n+1) = 1 := by
57   simp [alternating]
58 
59 theorem sampled_alternating_vanishes :
60     Tendsto (fun n => alternating (2*n)) atTop (𝓝 0) := by
61   simpa only [alternating_even] using (tendsto_const_nhds : Tendsto (fun _ : ℕ => (0 : ℝ)) atTop (𝓝 0))
62 
63 /-- Counterexample to unconditional residual-profile invariance under cofinal sampling. -/
64 theorem alternating_does_not_vanish : ¬ Tendsto alternating atTop (𝓝 0) := by
65   intro h
66   obtain ⟨N, hN⟩ := (Metric.tendsto_atTop.1 h) (1/2) (by norm_num)
67   have hh := hN (2*N+1) (by omega)
68   rw [alternating_odd] at hh
69   norm_num [Real.dist_eq] at hh
70 end Profiles
71 end KomorebiSpace

Back to source controls