1 include "arithmetics/sigma_pi.ma".
3 (************************* notation for minimization **************************)
4 notation "μ_{ ident i < n } p"
5 with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
7 notation "μ_{ ident i ≤ n } p"
8 with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
10 notation "μ_{ ident i ∈ [a,b[ } p"
11 with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
13 notation "μ_{ ident i ∈ [a,b] } p"
14 with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
16 (************************************ MAX *************************************)
17 notation "Max_{ ident i < n | p } f"
19 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
21 notation "Max_{ ident i < n } f"
23 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
25 notation "Max_{ ident j ∈ [a,b[ } f"
27 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
28 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
30 notation "Max_{ ident j ∈ [a,b[ | p } f"
32 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
33 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
35 lemma Max_assoc: ∀a,b,c. max (max a b) c = max a (max b c).
36 #a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
37 [cases (true_or_false (leb b c )) #lebc >lebc normalize
38 [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
41 |cases (true_or_false (leb b c )) #lebc >lebc normalize //
42 >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le
43 @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
47 lemma Max0 : ∀n. max 0 n = n.
50 lemma Max0r : ∀n. max n 0 = n.
51 #n >commutative_max //
55 mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
57 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
59 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
60 f a ≤ Max_{i < n | p i}(f i).
62 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
65 lemma le_MaxI: ∀f,p,n,m,a. m ≤ a → a < n → p a = true →
66 f a ≤ Max_{i ∈ [m,n[ | p i}(f i).
67 #f #p #n #m #a #lema #ltan #pa
68 >(bigop_diff ? ? 0 MaxAC (λi.f (i+m)) (a-m) (n-m))
69 [<plus_minus_m_m // @(le_maxl … (le_n ?))
71 |/2 by monotonic_lt_minus_l/
75 lemma Max_le: ∀f,p,n,b.
76 (∀a.a < n → p a = true → f a ≤ b) → Max_{i < n | p i}(f i) ≤ b.
77 #f #p #n elim n #b #H //
78 #b0 #H1 cases (true_or_false (p b)) #Hb
79 [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
80 |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
85 (************************* a couple of technical lemmas ***********************)
86 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
87 #a elim a // #n #Hind *
88 [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
91 lemma sigma_const: ∀c,a,b.
92 ∑_{i ∈ [a,b[ }c ≤ (b-a)*c.
93 #c #a #b elim (b-a) // #n #Hind normalize @le_plus //
96 lemma sigma_to_Max: ∀h,a,b.
97 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*Max_{i ∈ [a,b[ }(h i).
100 |#n #Hind >bigop_Strue [2://] whd in ⊢ (??%);
102 [>bigop_Strue // @(le_maxl … (le_n …))
103 |@(transitive_le … Hind) @le_times // >bigop_Strue //
104 @(le_maxr … (le_n …))
109 lemma sigma_bound1: ∀h,a,b. monotonic nat le h →
110 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*h b.
112 @(transitive_le … (sigma_to_Max …)) @le_times //
113 @Max_le #i #lti #_ @H @lt_to_le @lt_minus_to_plus_r //
116 lemma sigma_bound_decr1: ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
117 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*h a.
119 @(transitive_le … (sigma_to_Max …)) @le_times //
120 @Max_le #i #lti #_ @H // @lt_minus_to_plus_r //
123 lemma sigma_bound: ∀h,a,b. monotonic nat le h →
124 ∑_{i ∈ [a,S b[ }(h i) ≤ (S b-a)*h b.
125 #h #a #b #H cases (decidable_le a b)
126 [#leab cut (b = pred (S b - a + a))
127 [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
128 generalize in match (S b -a);
131 |#m #Hind >bigop_Strue [2://] @le_plus
132 [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
134 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
135 cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
139 lemma sigma_bound_decr: ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
140 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*h a.
141 #h #a #b #H cases (decidable_le a b)
142 [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
145 |#m #Hind >bigop_Strue [2://] #Hm
146 cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
147 @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
149 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
150 cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //