matita/matita/lib/reverse_complexity/sigma_diseq.ma

   1 include "arithmetics/sigma_pi.ma".
   2
   3 (************************* notation for minimization **************************)
   4 notation "μ_{ ident i < n } p"
   5   with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
   6
   7 notation "μ_{ ident i ≤ n } p"
   8   with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
   9
  10 notation "μ_{ ident i ∈ [a,b[ } p"
  11   with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
  12
  13 notation "μ_{ ident i ∈ [a,b] } p"
  14   with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
  15
  16 (************************************ MAX *************************************)
  17 notation "Max_{ ident i < n | p } f"
  18   with precedence 80
  19 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
  20
  21 notation "Max_{ ident i < n } f"
  22   with precedence 80
  23 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
  24
  25 notation "Max_{ ident j ∈ [a,b[ } f"
  26   with precedence 80
  27 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  28   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  29
  30 notation "Max_{ ident j ∈ [a,b[ | p } f"
  31   with precedence 80
  32 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  33   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  34
  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 //
  39     |>leab //
  40     ]
  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 //
  44   ]
  45 qed.
  46
  47 lemma Max0 : ∀n. max 0 n = n.
  48 // qed.
  49
  50 lemma Max0r : ∀n. max n 0 = n.
  51 #n >commutative_max //
  52 qed.
  53
  54 definition MaxA ≝
  55   mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
  56
  57 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
  58
  59 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
  60   f a ≤  Max_{i < n | p i}(f i).
  61 #f #p #n #a #ltan #pa
  62 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
  63 qed.
  64
  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 ?))
  70   |<plus_minus_m_m //
  71   |/2 by monotonic_lt_minus_l/
  72   ]
  73 qed.
  74
  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 //
  81   ]
  82 qed.
  83
  84
  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/]
  89 qed.
  90
  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 //
  94 qed.
  95
  96 lemma sigma_to_Max:  ∀h,a,b.
  97   ∑_{i ∈ [a,b[ }(h i) ≤  (b-a)*Max_{i ∈ [a,b[ }(h i).
  98 #h #a #b elim (b-a)
  99   [//
 100   |#n #Hind >bigop_Strue [2://] whd in ⊢ (??%);
 101    @le_plus
 102     [>bigop_Strue // @(le_maxl … (le_n …))
 103     |@(transitive_le … Hind) @le_times // >bigop_Strue //
 104      @(le_maxr … (le_n …))
 105     ]
 106   ]
 107 qed.
 108
 109 lemma sigma_bound1:  ∀h,a,b. monotonic nat le h →
 110   ∑_{i ∈ [a,b[ }(h i) ≤  (b-a)*h b.
 111 #h #a #b #H
 112 @(transitive_le … (sigma_to_Max …)) @le_times //
 113 @Max_le #i #lti #_ @H @lt_to_le @lt_minus_to_plus_r //
 114 qed.
 115
 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.
 118 #h #a #b #H
 119 @(transitive_le … (sigma_to_Max …)) @le_times //
 120 @Max_le #i #lti #_ @H // @lt_minus_to_plus_r //
 121 qed.
 122
 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);
 129    #n elim n
 130     [//
 131     |#m #Hind >bigop_Strue [2://] @le_plus
 132       [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
 133     ]
 134   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 135    cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
 136   ]
 137 qed.
 138
 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);
 143    #n elim n
 144     [//
 145     |#m #Hind >bigop_Strue [2://] #Hm
 146      cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
 147      @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
 148     ]
 149   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 150    cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
 151   ]
 152 qed.
 153