ContinuousPrecision.lean

1 module
2 public import Mathlib.Analysis.SpecialFunctions.Log.Basic
3 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
4 public import Mathlib.Tactic
5 
6 /-!
7 Author: Komorebi P.
8 Paper VIII 8.4, with the positive-budget hypothesis established in block one.
9 This proves feasibility, global optimality, and uniqueness of the actual log
10 objective. It does not assume stationary-point optimality or a KKT oracle.
11 -/
12 public section
13 set_option autoImplicit false
14 namespace KomorebiPaperVIII
15 open scoped BigOperators
16 variable {E : Type*} [Fintype E]
17 
18 noncomputable def precisionObjective (c eps : E → ℝ) : ℝ :=
19   ∑ e, c e * Real.log (1 / eps e)
20 
21 noncomputable def optimalTolerance (s c : E → ℝ) (budget : ℝ) (e : E) : ℝ :=
22   budget * c e / (s e * ∑ f, c f)
23 
24 def AllocationFeasible (s : E → ℝ) (budget : ℝ) (eps : E → ℝ) : Prop :=
25   (∀ e, 0 < eps e) ∧ ∑ e, s e * eps e = budget
26 
27 theorem total_cost_positive [Nonempty E] (c : E → ℝ) (hc : ∀ e, 0 < c e) :
28     0 < ∑ e, c e := by
29   exact Finset.sum_pos (fun e _ => hc e) Finset.univ_nonempty
30 
31 theorem optimal_tolerance_positive [Nonempty E] (s c : E → ℝ) (budget : ℝ)
32     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hb : 0 < budget) (e : E) :
33     0 < optimalTolerance s c budget e := by
34   exact div_pos (mul_pos hb (hc e)) (mul_pos (hs e) (total_cost_positive c hc))
35 
36 theorem optimal_tolerance_budget [Nonempty E] (s c : E → ℝ) (budget : ℝ)
37     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) :
38     ∑ e, s e * optimalTolerance s c budget e = budget := by
39   have hC : (∑ e, c e) ≠ 0 := ne_of_gt (total_cost_positive c hc)
40   have he : ∀ e, s e * optimalTolerance s c budget e = (budget / ∑ f, c f) * c e := by
41     intro e
42     dsimp [optimalTolerance]
43     field_simp [ne_of_gt (hs e)]
44   simp_rw [he]
45   rw [← Finset.mul_sum]
46   field_simp
47 
48 theorem optimal_tolerance_feasible [Nonempty E] (s c : E → ℝ) (budget : ℝ)
49     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hb : 0 < budget) :
50     AllocationFeasible s budget (optimalTolerance s c budget) := by
51   exact ⟨optimal_tolerance_positive s c budget hs hc hb,
52     optimal_tolerance_budget s c budget hs hc⟩
53 
54 theorem relative_budget_identity [Nonempty E] (s c eps : E → ℝ) (budget : ℝ)
55     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hb : 0 < budget)
56     (heps : ∑ e, s e * eps e = budget) :
57     ∑ e, c e * (eps e / optimalTolerance s c budget e) = ∑ e, c e := by
58   have hC : (∑ e, c e) ≠ 0 := ne_of_gt (total_cost_positive c hc)
59   have he : ∀ e, c e * (eps e / optimalTolerance s c budget e) =
60       ((∑ f, c f) / budget) * (s e * eps e) := by
61     intro e
62     dsimp [optimalTolerance]
63     field_simp [ne_of_gt (hs e), ne_of_gt (hc e), ne_of_gt hb]
64   simp_rw [he]
65   rw [← Finset.mul_sum, heps]
66   field_simp [ne_of_gt hb]
67 
68 theorem precision_objective_difference (c eps opt : E → ℝ)
69     (heps : ∀ e, 0 < eps e) (hopt : ∀ e, 0 < opt e) :
70     precisionObjective c eps - precisionObjective c opt =
71       -(∑ e, c e * Real.log (eps e / opt e)) := by
72   simp only [precisionObjective, one_div, Real.log_inv, ← Finset.sum_sub_distrib,
73     ← Finset.sum_neg_distrib]
74   apply Finset.sum_congr rfl
75   intro e _
76   rw [Real.log_div (ne_of_gt (heps e)) (ne_of_gt (hopt e))]
77   ring
78 
79 /-- Global lower bound from log(x) <= x-1, not a first-order heuristic. -/
80 theorem precision_allocation_optimal [Nonempty E] (s c : E → ℝ) (budget : ℝ)
81     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hb : 0 < budget)
82     (eps : E → ℝ) (heps : AllocationFeasible s budget eps) :
83     precisionObjective c (optimalTolerance s c budget) ≤ precisionObjective c eps := by
84   have ho := optimal_tolerance_positive s c budget hs hc hb
85   have hbalance := relative_budget_identity s c eps budget hs hc hb heps.2
86   have hlog : (∑ e, c e * Real.log (eps e / optimalTolerance s c budget e)) ≤ 0 := by
87     calc
88       _ ≤ ∑ e, c e * (eps e / optimalTolerance s c budget e - 1) := by
89         apply Finset.sum_le_sum
90         intro e _
91         exact mul_le_mul_of_nonneg_left
92           (Real.log_le_sub_one_of_pos (div_pos (heps.1 e) (ho e))) (le_of_lt (hc e))
93       _ = 0 := by
94         simp_rw [mul_sub, mul_one]
95         rw [Finset.sum_sub_distrib, hbalance, sub_self]
96   have hd := precision_objective_difference c eps (optimalTolerance s c budget) heps.1 ho
97   linarith
98 
99 /-- Every distinct feasible vector has strictly larger objective. -/
100 theorem precision_allocation_strict [Nonempty E] (s c : E → ℝ) (budget : ℝ)
101     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hb : 0 < budget)
102     (eps : E → ℝ) (heps : AllocationFeasible s budget eps)
103     (hne : eps ≠ optimalTolerance s c budget) :
104     precisionObjective c (optimalTolerance s c budget) < precisionObjective c eps := by
105   classical
106   have ho := optimal_tolerance_positive s c budget hs hc hb
107   have hbalance := relative_budget_identity s c eps budget hs hc hb heps.2
108   obtain ⟨e, he⟩ : ∃ e, eps e ≠ optimalTolerance s c budget e := by
109     by_contra hh
110     push Not at hh
111     exact hne (funext hh)
112   have hratio : eps e / optimalTolerance s c budget e ≠ 1 := by
113     intro hh
114     exact he ((div_eq_one_iff_eq (ne_of_gt (ho e))).1 hh)
115   have hlog : (∑ e, c e * Real.log (eps e / optimalTolerance s c budget e)) < 0 := by
116     calc
117       _ < ∑ e, c e * (eps e / optimalTolerance s c budget e - 1) := by
118         apply Finset.sum_lt_sum
119         · intro i _
120           exact mul_le_mul_of_nonneg_left
121             (Real.log_le_sub_one_of_pos (div_pos (heps.1 i) (ho i))) (le_of_lt (hc i))
122         · exact ⟨e, Finset.mem_univ e, mul_lt_mul_of_pos_left
123             (Real.log_lt_sub_one_of_pos (div_pos (heps.1 e) (ho e)) hratio) (hc e)⟩
124       _ = 0 := by
125         simp_rw [mul_sub, mul_one]
126         rw [Finset.sum_sub_distrib, hbalance, sub_self]
127   have hd := precision_objective_difference c eps (optimalTolerance s c budget) heps.1 ho
128   linarith
129 
130 /-- The stated formula is the unique feasible global minimizer. -/
131 theorem continuous_precision_unique_minimizer [Nonempty E] (s c : E → ℝ) (budget : ℝ)
132     (hs : ∀ e, 0 < s e) (hc : ∀ e, 0 < c e) (hb : 0 < budget) :
133     AllocationFeasible s budget (optimalTolerance s c budget) ∧
134     ∀ eps : E → ℝ, AllocationFeasible s budget eps →
135       ((∀ other : E → ℝ, AllocationFeasible s budget other →
136           precisionObjective c eps ≤ precisionObjective c other) ↔
137         eps = optimalTolerance s c budget) := by
138   constructor
139   · exact optimal_tolerance_feasible s c budget hs hc hb
140   · intro eps heps
141     constructor
142     · intro hmin
143       by_contra hne
144       have hlt := precision_allocation_strict s c budget hs hc hb eps heps hne
145       have hle := hmin _ (optimal_tolerance_feasible s c budget hs hc hb)
146       linarith
147     · intro h
148       subst eps
149       exact precision_allocation_optimal s c budget hs hc hb
150 
151 end KomorebiPaperVIII
152 
153 -- FINAL AXIOM AUDITS
154 #print axioms KomorebiPaperVIII.total_cost_positive
155 #print axioms KomorebiPaperVIII.optimal_tolerance_positive
156 #print axioms KomorebiPaperVIII.optimal_tolerance_budget
157 #print axioms KomorebiPaperVIII.optimal_tolerance_feasible
158 #print axioms KomorebiPaperVIII.relative_budget_identity
159 #print axioms KomorebiPaperVIII.precision_objective_difference
160 #print axioms KomorebiPaperVIII.precision_allocation_optimal
161 #print axioms KomorebiPaperVIII.precision_allocation_strict
162 #print axioms KomorebiPaperVIII.continuous_precision_unique_minimizer
163 #print axioms KomorebiPaperVIII.optimalTolerance

Back to source controls