ObstructionFloor.lean

1 import Mathlib.Topology.MetricSpace.HausdorffDistance
2 import Mathlib.Analysis.Normed.Group.Basic
3 import Mathlib.Algebra.Group.Subgroup.Basic
4 import Mathlib.Tactic.Linarith
5 
6 set_option autoImplicit false
7 
8 /-!
9 # The irreducible residual floor
10 
11 Distance zero means membership in the closure of admissible boundaries. Actual
12 flattening follows only if this boundary subgroup is closed.
13 -/
14 universe u
15 namespace KomorebiSpace
16 namespace ObstructionFloor
17 open Filter
18 open scoped Topology
19 variable {R : Type u} [NormedAddCommGroup R]
20 
21 noncomputable def floor (B : AddSubgroup R) (ω : R) : ℝ := Metric.infDist ω (B : Set R)
22 
23 theorem nonnegative (B : AddSubgroup R) (ω : R) : 0 ≤ floor B ω := Metric.infDist_nonneg
24 
25 theorem lower_bound (B : AddSubgroup R) (ω a : R) (ha : a ∈ B) :
26     floor B ω ≤ ‖ω-a‖ := by
27   simpa only [floor, dist_eq_norm] using (Metric.infDist_le_dist_of_mem (x := ω) ha)
28 
29 theorem zero_iff_closure (B : AddSubgroup R) (ω : R) :
30     floor B ω = 0 ↔ ω ∈ closure (B : Set R) :=
31   (Metric.mem_closure_iff_infDist_zero (s := (B : Set R)) ⟨0, B.zero_mem⟩).symm
32 
33 theorem zero_iff_mem_of_closed (B : AddSubgroup R) (hB : IsClosed (B : Set R)) (ω : R) :
34     floor B ω = 0 ↔ ω ∈ B := by
35   rw [zero_iff_closure, hB.closure_eq]
36   rfl
37 
38 /-- Every sequence of admissible corrections is blocked by a persistent positive floor. -/
39 theorem persistent_obstruction (B : ℕ → AddSubgroup R) (Ω a : ℕ → R)
40     (ha : ∀ n, a n ∈ B n) (c : ℝ) (hc : 0 < c)
41     (hfloor : ∀ᶠ n in atTop, c ≤ floor (B n) (Ω n)) :
42     ¬ Tendsto (fun n => ‖Ω n-a n‖) atTop (𝓝 0) := by
43   intro hv
44   have hle : c ≤ 0 := ge_of_tendsto hv
45     (hfloor.mono fun n hn => hn.trans (lower_bound (B n) (Ω n) (a n) (ha n)))
46   linarith
47 
48 end ObstructionFloor
49 end KomorebiSpace

Back to source controls