MonotoneBudgetAsymptotic.lean

1 import Mathlib.Analysis.SpecificLimits.Basic
2 import Mathlib.Tactic
3 
4 set_option autoImplicit false
5 noncomputable section
6 open Filter Set
7 open scoped Topology
8 
9 namespace KomorebiSpace.DiagonalRegularization
10 
11 /-- Any budget above the initial mesh value lies between consecutive mesh values. -/
12 lemma exists_budget_mesh_bracket (u : ℕ → ℝ)
13     (hu : Tendsto u atTop atTop) (M : ℝ) (hM : u 0 ≤ M) :
14     ∃ n : ℕ, u n ≤ M ∧ M < u (n + 1) := by
15   have he : ∃ n : ℕ, M < u n := (hu.eventually (eventually_gt_atTop M)).exists
16   let k := Nat.find he
17   have hk : M < u k := Nat.find_spec he
18   have hkpos : 0 < k := by
19     by_contra h
20     have hkzero : k = 0 := by omega
21     rw [hkzero] at hk
22     linarith
23   have hmin : ¬M < u (k - 1) := Nat.find_min he (by change k - 1 < k; omega)
24   refine ⟨k - 1, le_of_not_gt hmin, ?_⟩
25   have heq : k - 1 + 1 = k := by omega
26   simpa only [heq] using hk
27 
28 /-- A bracket index for every real budget, with the irrelevant initial segment assigned zero. -/
29 def budgetMeshIndex (u : ℕ → ℝ) (hu : Tendsto u atTop atTop) (M : ℝ) : ℕ :=
30   if hM : u 0 ≤ M then Classical.choose (exists_budget_mesh_bracket u hu M hM) else 0
31 
32 lemma budgetMeshIndex_bracket (u : ℕ → ℝ) (hu : Tendsto u atTop atTop)
33     (M : ℝ) (hM : u 0 ≤ M) :
34     u (budgetMeshIndex u hu M) ≤ M ∧ M < u (budgetMeshIndex u hu M + 1) := by
35   unfold budgetMeshIndex
36   rw [dite_eq_left hM]
37   exact Classical.choose_spec (exists_budget_mesh_bracket u hu M hM)
38 
39 lemma budgetMeshIndex_tendsto (u : ℕ → ℝ) (hmono : Monotone u)
40     (hu : Tendsto u atTop atTop) : Tendsto (budgetMeshIndex u hu) atTop atTop := by
41   refine tendsto_atTop_atTop.mpr fun N => ⟨max (u 0) (u N), fun M hM => ?_⟩
42   have hMzero : u 0 ≤ M := le_trans (le_max_left _ _) hM
43   have hMN : u N ≤ M := le_trans (le_max_right _ _) hM
44   have hb := (budgetMeshIndex_bracket u hu M hMzero).2
45   by_contra h
46   have hle : budgetMeshIndex u hu M + 1 ≤ N := by omega
47   have hm := hmono hle
48   linarith
49 
50 lemma tendsto_budget_mesh_lower (u : ℕ → ℝ) (β : ℝ → ℝ) (c : ℝ)
51     (hpos : ∀ n, 0 < u n)
52     (hratio : Tendsto (fun n => u (n + 1) / u n) atTop (𝓝 1))
53     (hprod : Tendsto (fun n => u n * β (u n)) atTop (𝓝 c)) :
54     Tendsto (fun n => u n * β (u (n + 1))) atTop (𝓝 c) := by
55   have hshift := hprod.comp (tendsto_add_atTop_nat 1)
56   have hlim : Tendsto (fun n => (u (n + 1) / u n)⁻¹ *
57       (u (n + 1) * β (u (n + 1)))) atTop (𝓝 c) := by
58     simpa only [Pi.mul_def, Pi.inv_def, Function.comp_def, inv_one, one_mul] using
59       (hratio.inv₀ (by norm_num : (1 : ℝ) ≠ 0)).mul hshift
60   apply hlim.congr'
61   exact Eventually.of_forall (fun n => by
62     field_simp [ne_of_gt (hpos n), ne_of_gt (hpos (n + 1))])
63 
64 lemma tendsto_budget_mesh_upper (u : ℕ → ℝ) (β : ℝ → ℝ) (c : ℝ)
65     (hpos : ∀ n, 0 < u n)
66     (hratio : Tendsto (fun n => u (n + 1) / u n) atTop (𝓝 1))
67     (hprod : Tendsto (fun n => u n * β (u n)) atTop (𝓝 c)) :
68     Tendsto (fun n => u (n + 1) * β (u n)) atTop (𝓝 c) := by
69   have hlim : Tendsto (fun n => (u (n + 1) / u n) * (u n * β (u n)))
70       atTop (𝓝 c) := by
71     simpa only [Pi.mul_def, one_mul] using hratio.mul hprod
72   apply hlim.congr'
73   exact Eventually.of_forall (fun n => by field_simp [ne_of_gt (hpos n)])
74 
75 /-- Convergence on a positive asymptotically fine monotone budget mesh determines the full
76 real-budget limit for any nonnegative antitone profile. -/
77 theorem tendsto_budget_product_of_mesh (u : ℕ → ℝ) (β : ℝ → ℝ) (c : ℝ)
78     (hpos : ∀ n, 0 < u n) (hmono : Monotone u) (hu : Tendsto u atTop atTop)
79     (hβmono : AntitoneOn β (Ici 0)) (hβnonneg : ∀ M, 0 ≤ M → 0 ≤ β M)
80     (hratio : Tendsto (fun n => u (n + 1) / u n) atTop (𝓝 1))
81     (hprod : Tendsto (fun n => u n * β (u n)) atTop (𝓝 c)) :
82     Tendsto (fun M : ℝ => M * β M) atTop (𝓝 c) := by
83   have hi := budgetMeshIndex_tendsto u hmono hu
84   have hlo := (tendsto_budget_mesh_lower u β c hpos hratio hprod).comp hi
85   have hup := (tendsto_budget_mesh_upper u β c hpos hratio hprod).comp hi
86   apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hlo hup
87   · filter_upwards [eventually_ge_atTop (u 0)] with M hM
88     have hb := budgetMeshIndex_bracket u hu M hM
89     have hMnonneg : 0 ≤ M := le_trans (hpos 0).le hM
90     have hβle : β (u (budgetMeshIndex u hu M + 1)) ≤ β M :=
91       hβmono hMnonneg (hpos _).le hb.2.le
92     exact mul_le_mul hb.1 hβle (hβnonneg _ (hpos _).le) hMnonneg
93   · filter_upwards [eventually_ge_atTop (u 0)] with M hM
94     have hb := budgetMeshIndex_bracket u hu M hM
95     have hMnonneg : 0 ≤ M := le_trans (hpos 0).le hM
96     have hβle : β M ≤ β (u (budgetMeshIndex u hu M)) :=
97       hβmono (hpos _).le hMnonneg hb.1
98     exact mul_le_mul hb.2.le hβle (hβnonneg M hMnonneg) (hpos _).le
99 
100 end KomorebiSpace.DiagonalRegularization

Back to source controls