ClippedPrecision.lean

1 module
2 public import ContinuousPrecision
3 import all ContinuousPrecision
4 public import Mathlib.Topology.Order.IntermediateValue
5 public import Mathlib.Tactic
6 
7 /-!
8 Author: Komorebi P.
9 Paper VIII 8.5. A continuous capped water-filling construction, including
10 existence, global optimality, uniqueness of the vector, and the multiplier
11 boundary. The scale t is the reciprocal of the manuscript's multiplier.
12 -/
13 @[expose] public section
14 set_option autoImplicit false
15 namespace KomorebiPaperVIII
16 open scoped BigOperators
17 variable {E : Type*} [Fintype E]
18 
19 noncomputable def clippedTolerance (s c m : E → ℝ) (t : ℝ) (e : E) : ℝ :=
20   min (m e) (t * (c e / s e))
21 
22 noncomputable def clippedTotal (s c m : E → ℝ) (t : ℝ) : ℝ :=
23   ∑ e, s e * clippedTolerance s c m t e
24 
25 def ClippedFeasible (s m : E → ℝ) (budget : ℝ) (eps : E → ℝ) : Prop :=
26   AllocationFeasible s budget eps ∧ ∀ e, eps e ≤ m e
27 
28 omit [Fintype E] in
29 theorem clipped_positive (s c m : E → ℝ) (t : ℝ)
30     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e)
31     (ht : 0 < t) (e : E) : 0 < clippedTolerance s c m t e := by
32   exact lt_min (hm e) (mul_pos ht (div_pos (hc e) (hs e)))
33 
34 theorem clipped_total_continuous (s c m : E → ℝ) : Continuous (clippedTotal s c m) := by
35   unfold clippedTotal clippedTolerance
36   fun_prop
37 
38 theorem clipped_total_mono (s c m : E → ℝ)
39     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) : Monotone (clippedTotal s c m) := by
40   intro t u htu
41   apply Finset.sum_le_sum
42   intro e _
43   exact mul_le_mul_of_nonneg_left
44     (min_le_min_left _ (mul_le_mul_of_nonneg_right htu (le_of_lt (div_pos (hc e) (hs e)))))
45     (le_of_lt (hs e))
46 
47 theorem clipped_total_zero (s c m : E → ℝ) (hm : ∀ e, 0 < m e) :
48     clippedTotal s c m 0 = 0 := by
49   simp [clippedTotal, clippedTolerance, le_of_lt (hm _)]
50 
51 /-- A finite positive scale at which every coordinate is saturated. -/
52 noncomputable def saturationScale (s c m : E → ℝ) : ℝ := ∑ e, m e * s e / c e
53 
54 theorem saturation_scale_positive [Nonempty E] (s c m : E → ℝ)
55     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e) :
56     0 < saturationScale s c m := by
57   exact Finset.sum_pos (fun e _ => div_pos (mul_pos (hm e) (hs e)) (hc e))
58     Finset.univ_nonempty
59 
60 theorem saturation_scale_attains (s c m : E → ℝ)
61     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e) :
62     clippedTolerance s c m (saturationScale s c m) = m := by
63   funext e
64   apply min_eq_left
65   have he : m e * s e / c e ≤ saturationScale s c m :=
66     Finset.single_le_sum (fun i _ => le_of_lt (div_pos (mul_pos (hm i) (hs i)) (hc i)))
67       (Finset.mem_univ e)
68   have h := mul_le_mul_of_nonneg_right he (le_of_lt (div_pos (hc e) (hs e)))
69   have hcancel : (m e * s e / c e) * (c e / s e) = m e := by
70     field_simp [(hs e).ne', (hc e).ne']
71   rwa [hcancel] at h
72 
73 /-- IVT supplies a scale from the budget itself; no multiplier is assumed. -/
74 theorem clipped_scale_exists [Nonempty E] (s c m : E → ℝ) (budget : ℝ)
75     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e)
76     (hb : 0 < budget) (hcap : budget ≤ ∑ e, s e * m e) :
77     ∃ t, 0 < t ∧ clippedTotal s c m t = budget := by
78   have hT := saturation_scale_positive s c m hs hc hm
79   have hend : clippedTotal s c m (saturationScale s c m) = ∑ e, s e * m e := by
80     simp only [clippedTotal, saturation_scale_attains s c m hs hc hm]
81   have hmem : budget ∈ Set.Icc (clippedTotal s c m 0)
82       (clippedTotal s c m (saturationScale s c m)) := by
83     rw [clipped_total_zero s c m hm, hend]
84     exact ⟨hb.le, hcap⟩
85   obtain ⟨t, ht, heq⟩ := intermediate_value_Icc hT.le
86     (clipped_total_continuous s c m).continuousOn hmem
87   refine ⟨t, ?_, heq⟩
88   by_contra hn
89   have ht0 : t = 0 := le_antisymm (le_of_not_gt hn) ht.1
90   subst t
91   rw [clipped_total_zero s c m hm] at heq
92   linarith
93 
94 /-- Strict increase holds below saturation, not on the constant endpoint ray. -/
95 theorem clipped_total_strict_below_cap (s c m : E → ℝ)
96     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (t u : ℝ) (htu : t < u)
97     (hbelow : clippedTotal s c m t < ∑ e, s e * m e) :
98     clippedTotal s c m t < clippedTotal s c m u := by
99   classical
100   obtain ⟨e, he⟩ : ∃ e, clippedTolerance s c m t e < m e := by
101     by_contra hh
102     push Not at hh
103     have hall : ∀ e, clippedTolerance s c m t e = m e :=
104       fun e => le_antisymm (min_le_left _ _) (hh e)
105     simp only [clippedTotal, hall] at hbelow
106     exact lt_irrefl _ hbelow
107   apply Finset.sum_lt_sum
108   · intro i _
109     exact mul_le_mul_of_nonneg_left
110       (min_le_min_left _ (mul_le_mul_of_nonneg_right htu.le (le_of_lt (div_pos (hc i) (hs i)))))
111       (hs i).le
112   · refine ⟨e, Finset.mem_univ e, mul_lt_mul_of_pos_left ?_ (hs e)⟩
113     exact lt_min he (lt_of_le_of_lt (min_le_right _ _)
114       (mul_lt_mul_of_pos_right htu (div_pos (hc e) (hs e))))
115 
116 theorem clipped_scale_unique (s c m : E → ℝ) (budget : ℝ)
117     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e)
118     (hcap : budget < ∑ e, s e * m e) (t u : ℝ)
119     (ht : clippedTotal s c m t = budget) (hu : clippedTotal s c m u = budget) : t = u := by
120   apply le_antisymm
121   · by_contra h
122     have hl := clipped_total_strict_below_cap s c m hs hc u t (lt_of_not_ge h)
123       (by simpa [hu] using hcap)
124     linarith
125   · by_contra h
126     have hl := clipped_total_strict_below_cap s c m hs hc t u (lt_of_not_ge h)
127       (by simpa [ht] using hcap)
128     linarith
129 
130 /-- Coordinate supporting inequality, including saturated coordinates. -/
131 theorem clipped_supporting_inequality (s c m t x : ℝ)
132     (hs : 0 < s) (hc : 0 < c) (hm : 0 < m) (ht : 0 < t) (hx : x ≤ m) :
133     c * (x / min m (t * (c/s)) - 1) ≤ (s/t) * (x - min m (t * (c/s))) := by
134   by_cases h : m ≤ t * (c/s)
135   · rw [min_eq_left h]
136     have hcross : s*m ≤ c*t := by
137       have hh : m*s ≤ t*c := (le_div_iff₀ hs).1 (by simpa [mul_div_assoc] using h)
138       nlinarith
139     have hcoef : s/t ≤ c/m := (div_le_div_iff₀ ht hm).2 hcross
140     have hi := mul_le_mul_of_nonpos_right hcoef (sub_nonpos.mpr hx)
141     have hid : c*(x/m-1) = (c/m)*(x-m) := by field_simp
142     rwa [← hid] at hi
143   · rw [min_eq_right (le_of_not_ge h)]
144     have hid : c * (x / (t*(c/s)) - 1) = (s/t) * (x - t*(c/s)) := by
145       field_simp
146     exact hid.le
147 
148 /-- The tangent bound sums to zero for every feasible clipped competitor. -/
149 theorem clipped_relative_sum_le_zero (s c m : E → ℝ) (budget t : ℝ)
150     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e)
151     (ht : 0 < t) (hbudget : clippedTotal s c m t = budget)
152     (eps : E → ℝ) (heps : ClippedFeasible s m budget eps) :
153     ∑ e, c e * (eps e / clippedTolerance s c m t e - 1) ≤ 0 := by
154   calc
155     _ ≤ ∑ e, (s e/t) * (eps e-clippedTolerance s c m t e) := by
156       apply Finset.sum_le_sum
157       intro e _
158       exact clipped_supporting_inequality _ _ _ _ _ (hs e) (hc e) (hm e) ht (heps.2 e)
159     _ = 0 := by
160       simp_rw [div_mul_eq_mul_div, mul_sub]
161       rw [← Finset.sum_div, Finset.sum_sub_distrib, heps.1.2]
162       change (budget - clippedTotal s c m t) / t = 0
163       rw [hbudget, sub_self, zero_div]
164 
165 theorem clipped_allocation_optimal (s c m : E → ℝ) (budget t : ℝ)
166     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e)
167     (ht : 0 < t) (hbudget : clippedTotal s c m t = budget)
168     (eps : E → ℝ) (heps : ClippedFeasible s m budget eps) :
169     precisionObjective c (clippedTolerance s c m t) ≤ precisionObjective c eps := by
170   have ho := clipped_positive s c m t hs hc hm ht
171   have hlog : (∑ e, c e * Real.log (eps e / clippedTolerance s c m t e)) ≤ 0 := by
172     calc
173       _ ≤ ∑ e, c e * (eps e / clippedTolerance s c m t e - 1) := by
174         apply Finset.sum_le_sum
175         intro e _
176         exact mul_le_mul_of_nonneg_left
177           (Real.log_le_sub_one_of_pos (div_pos (heps.1.1 e) (ho e))) (hc e).le
178       _ ≤ 0 := clipped_relative_sum_le_zero s c m budget t hs hc hm ht hbudget eps heps
179   have hd := precision_objective_difference c eps (clippedTolerance s c m t) heps.1.1 ho
180   linarith
181 
182 theorem clipped_allocation_strict (s c m : E → ℝ) (budget t : ℝ)
183     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e)
184     (ht : 0 < t) (hbudget : clippedTotal s c m t = budget)
185     (eps : E → ℝ) (heps : ClippedFeasible s m budget eps)
186     (hne : eps ≠ clippedTolerance s c m t) :
187     precisionObjective c (clippedTolerance s c m t) < precisionObjective c eps := by
188   classical
189   have ho := clipped_positive s c m t hs hc hm ht
190   obtain ⟨e, he⟩ : ∃ e, eps e ≠ clippedTolerance s c m t e := by
191     by_contra h
192     push Not at h
193     exact hne (funext h)
194   have hr : eps e / clippedTolerance s c m t e ≠ 1 := by
195     intro h
196     exact he ((div_eq_one_iff_eq (ho e).ne').1 h)
197   have hlog : (∑ e, c e * Real.log (eps e / clippedTolerance s c m t e)) < 0 := by
198     calc
199       _ < ∑ e, c e * (eps e / clippedTolerance s c m t e - 1) := by
200         apply Finset.sum_lt_sum
201         · intro i _
202           exact mul_le_mul_of_nonneg_left
203             (Real.log_le_sub_one_of_pos (div_pos (heps.1.1 i) (ho i))) (hc i).le
204         · exact ⟨e, Finset.mem_univ e, mul_lt_mul_of_pos_left
205             (Real.log_lt_sub_one_of_pos (div_pos (heps.1.1 e) (ho e)) hr) (hc e)⟩
206       _ ≤ 0 := clipped_relative_sum_le_zero s c m budget t hs hc hm ht hbudget eps heps
207   have hd := precision_objective_difference c eps (clippedTolerance s c m t) heps.1.1 ho
208   linarith
209 
210 /-- Full feasibility and the unique minimizing vector at every positive feasible budget. -/
211 theorem clipped_unique_minimizer [Nonempty E] (s c m : E → ℝ) (budget : ℝ)
212     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e)
213     (hb : 0 < budget) (hcap : budget ≤ ∑ e, s e * m e) :
214     ∃ t, 0 < t ∧ ClippedFeasible s m budget (clippedTolerance s c m t) ∧
215       ∀ eps, ClippedFeasible s m budget eps →
216         ((∀ other, ClippedFeasible s m budget other →
217             precisionObjective c eps ≤ precisionObjective c other) ↔
218           eps = clippedTolerance s c m t) := by
219   obtain ⟨t, ht, heq⟩ := clipped_scale_exists s c m budget hs hc hm hb hcap
220   have hf : ClippedFeasible s m budget (clippedTolerance s c m t) :=
221     ⟨⟨clipped_positive s c m t hs hc hm ht, heq⟩, fun _ => min_le_left _ _⟩
222   refine ⟨t, ht, hf, ?_⟩
223   intro eps heps
224   constructor
225   · intro hmin
226     by_contra hne
227     have hl := clipped_allocation_strict s c m budget t hs hc hm ht heq eps heps hne
228     have hu := hmin _ hf
229     linarith
230   · intro h
231     subst eps
232     exact fun other hother => clipped_allocation_optimal s c m budget t hs hc hm ht heq other hother
233 
234 /- The parameter is the reciprocal of the manuscript's multiplier. -/
235 omit [Fintype E] in
236 theorem clipped_multiplier_formula (s c m : E → ℝ) (t : ℝ) (ht : 0 < t) :
237     clippedTolerance s c m t = fun e => min (m e) (c e / ((1/t)*s e)) := by
238   funext e
239   unfold clippedTolerance
240   congr 1
241   field_simp
242 
243 /-- At the endpoint different positive multipliers can give the same optimum. -/
244 theorem clipped_endpoint_nonunique_multiplier :
245     min (1 : ℝ) (1 / ((1:ℝ)*1)) = 1 ∧
246     min (1 : ℝ) (1 / (((1:ℝ)/2)*1)) = 1 ∧ (1:ℝ) ≠ 1/2 := by
247   norm_num
248 
249 /-- Unique positive manuscript multiplier at every strictly submaximal budget. -/
250 theorem clipped_multiplier_exists_unique [Nonempty E] (s c m : E → ℝ) (budget : ℝ)
251     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hm : ∀ e, 0 < m e)
252     (hb : 0 < budget) (hcap : budget < ∑ e, s e * m e) :
253     ∃! lambda : ℝ, 0 < lambda ∧
254       (∑ e, s e * min (m e) (c e / (lambda * s e))) = budget := by
255   obtain ⟨t, ht, heq⟩ := clipped_scale_exists s c m budget hs hc hm hb hcap.le
256   refine ⟨1/t, ⟨one_div_pos.mpr ht, ?_⟩, ?_⟩
257   · simpa only [clippedTotal, clipped_multiplier_formula s c m t ht] using heq
258   · intro mu hmu
259     have hu : clippedTotal s c m (1/mu) = budget := by
260       simpa only [clippedTotal, clipped_multiplier_formula s c m (1/mu) (one_div_pos.mpr hmu.1),
261         one_div_one_div] using hmu.2
262     have he := clipped_scale_unique s c m budget hs hc hcap (1/mu) t hu heq
263     have hr := congrArg (fun z : ℝ => 1/z) he
264     simpa only [one_div_one_div] using hr
265 
266 end KomorebiPaperVIII
267 
268 -- FINAL AXIOM AUDITS
269 #print axioms KomorebiPaperVIII.clipped_positive
270 #print axioms KomorebiPaperVIII.clipped_total_continuous
271 #print axioms KomorebiPaperVIII.clipped_total_mono
272 #print axioms KomorebiPaperVIII.clipped_total_zero
273 #print axioms KomorebiPaperVIII.saturation_scale_positive
274 #print axioms KomorebiPaperVIII.saturation_scale_attains
275 #print axioms KomorebiPaperVIII.clipped_scale_exists
276 #print axioms KomorebiPaperVIII.clipped_total_strict_below_cap
277 #print axioms KomorebiPaperVIII.clipped_scale_unique
278 #print axioms KomorebiPaperVIII.clipped_supporting_inequality
279 #print axioms KomorebiPaperVIII.clipped_relative_sum_le_zero
280 #print axioms KomorebiPaperVIII.clipped_allocation_optimal
281 #print axioms KomorebiPaperVIII.clipped_allocation_strict
282 #print axioms KomorebiPaperVIII.clipped_unique_minimizer
283 #print axioms KomorebiPaperVIII.clipped_multiplier_formula
284 #print axioms KomorebiPaperVIII.clipped_endpoint_nonunique_multiplier
285 
286 #print axioms KomorebiPaperVIII.clipped_multiplier_exists_unique
287 
288 #print axioms KomorebiPaperVIII.clippedTolerance
289 
290 #print axioms KomorebiPaperVIII.saturationScale

Back to source controls