amgm.lean

import tactic.basic
import tactic.apply
import tactic.ring
import tactic.abel
import tactic.linarith
import tactic.norm_num
import data.rat.basic
import data.rat.basic
import data.real.basic
import analysis.complex.exponential
import data.real.nnreal
import data.list.min_max
import init.algebra.order
import algebra.big_operators
import algebra.group_power

open list option nnreal
open_locale nnreal


theorem prod_remove_nth {α : Type*} [comm_monoid α] : ∀ (l : list α) (i : ℕ), (i < length l) → (remove_nth l i).prod * (l.nth_le i ‹_›) = l.prod
| []      _     h := absurd h (by simp only [not_lt, length, nat.zero_le])
| (x::xs) 0     h := by simp only [remove_nth, mul_comm, prod_cons, nth_le]
| (x::xs) (i+1) h := begin have : i < length xs, from nat.lt_of_succ_lt_succ h,
  dsimp [remove_nth],
  rw prod_cons,
  rw prod_cons,
  rw mul_assoc,
   erw [prod_remove_nth xs i this],
  end

theorem sum_remove_nth {α : Type*} [add_comm_monoid α] : ∀ (l : list α) (i : ℕ), (i < length l) → (remove_nth l i).sum + (l.nth_le i ‹_›) = l.sum
| []      _     h := absurd h (by simp only [not_lt, length, nat.zero_le])
| (x::xs) 0     h := by simp only [remove_nth, add_comm, sum_cons, nth_le]
| (x::xs) (i+1) h := begin have : i < length xs, from nat.lt_of_succ_lt_succ h,
  dsimp [remove_nth],
  rw sum_cons,
  rw sum_cons,
  rw add_assoc,
   erw [sum_remove_nth xs i this],
  end

theorem prod_update_nth {α : Type*} [comm_monoid α] : ∀ (l : list α) (i : ℕ), (i < length l) → α → (update_nth l i ‹_›).prod * (l.nth_le i ‹_›) = l.prod * (‹_› : α)
| []      _     h t := absurd h (by simp only [not_lt, list.length, nat.zero_le])
| (x::xs) 0     h t := begin simp [update_nth, prod_cons, list.nth_le], conv_lhs { rw mul_comm, congr, skip, rw mul_comm, }, rw mul_assoc, end
| (x::xs) (i+1) h t := begin have : i < length xs, from nat.lt_of_succ_lt_succ h,
  dsimp [update_nth],
  rw prod_cons,
  rw prod_cons,
  rw mul_assoc,
   erw [prod_update_nth xs i this],
  rw mul_assoc,
  end

theorem sum_update_nth {α : Type*} [add_comm_monoid α] : ∀ (l : list α) (i : ℕ), (i < length l) → α → (update_nth l i ‹_›).sum + (l.nth_le i ‹_›) = l.sum + (‹_› : α)
| []      _     h t := absurd h (by simp only [not_lt, list.length, nat.zero_le])
| (x::xs) 0     h t := begin simp [update_nth, sum_cons, list.nth_le], end
| (x::xs) (i+1) h t := begin have : i < length xs, from nat.lt_of_succ_lt_succ h,
  dsimp [update_nth],
  rw sum_cons,
  rw sum_cons,
  rw add_assoc,
   erw [sum_update_nth xs i this],
  rw add_assoc,
  end

lemma aux {x y : ℝ≥0} (hx : 1 ≤ x) (hy : y ≤ 1) : 1 ≤ x + y - x * y:=
begin
   have x_sub_one_nonneg : 0 ≤ (x : ℝ) - 1 := sub_nonneg_of_le hx,
   have one_sub_y_nonneg : 0 ≤ 1 - (y : ℝ) := sub_nonneg_of_le hy,
   have prod_expand : ((x : ℝ) - 1) * (1- y) = (↑x :ℝ) + (↑y + -(↑x * ↑y)) - 1 := by ring,
   have := mul_nonneg' x_sub_one_nonneg one_sub_y_nonneg,
   rw prod_expand at this,
   rw sub_nonneg at this,
   rw [← nnreal.coe_le, nnreal.coe_one, nnreal.coe_sub],
   simpa only [add_assoc, nnreal.coe_add, sub_eq_add_neg, nnreal.coe_mul] using this,
   rw [← nnreal.coe_le, nnreal.coe_add, nnreal.coe_mul],
   linarith,
end

lemma prod_elem_eq_zero_eq_zero {l : list ℝ≥0} (ha : (0 : ℝ≥0) ∈ l) : l.prod = 0 :=
begin
   induction l,
   simpa only [prod_nil, not_mem_nil, one_ne_zero] using ha,
   rw prod_cons,
   cases ha,
   rw [← ha, zero_mul],
   rw [l_ih ha, mul_zero],
end

lemma prod_ne_zero_elem_ne_zero {l : list ℝ≥0} (h : l.prod ≠ 0) {a : ℝ≥0} (ha : a ∈ l) : a ≠ 0 :=
assume t, by rw t at ha; exact h (prod_elem_eq_zero_eq_zero ha)

lemma prod_lt_one_lt_one {l : list ℝ≥0} (hl : l ≠ []) (hlt : ∀ (a : ℝ≥0) (ha : a ∈ l), a < 1) : l.prod < 1 :=
begin
   induction l,
   simpa only [prod_nil, not_true, ne.def, prod_nil, ne.def] using hl,
   rw prod_cons,
   have hd_lt_one := hlt l_hd (by simp),
   by_cases l_tl = [],
   simp only [h, hd_lt_one, prod_nil, mul_one],
   have := l_ih h (begin intros b hb, convert hlt b _, rw mem_cons_iff, simp only [hb, or_true], end),
   convert mul_lt_mul'' hd_lt_one this (zero_le _) (zero_le _),
   rw mul_one,
end

lemma prod_gt_one_gt_one {l : list ℝ≥0} (hl : l ≠ []) (hlt : ∀ (a : ℝ≥0) (ha : a ∈ l), 1 < a) : 1 < l.prod :=
begin
   induction l,
   simpa only [prod_nil, not_true, ne.def, prod_nil, ne.def] using hl,
   rw prod_cons,
   have hd_lt_one := hlt l_hd (by simp),
   by_cases l_tl = [],
   simp only [h, hd_lt_one, prod_nil, mul_one],
   have := l_ih h (begin intros b hb, convert hlt b _, rw mem_cons_iff, simp only [hb, or_true], end),
   convert mul_lt_mul'' hd_lt_one this (zero_le _) (zero_le _),
   rw mul_one,
end

lemma prod_ge_one_max_ge_one {l : list ℝ≥0} (hl : l ≠ []) (hlo : 1 ≤ l.prod) : 1 ≤ l.maximum :=
begin
   contrapose hlo,
   rw not_le at *,
   have : (∀ (a : ℝ≥0) (ha : a ∈ l), a < 1) :=
   begin
      intros b hb,
      rw [ne.def] at hl,
      rw ← maximum_eq_none at hl,
      change l.maximum ≠ none at hl,
      rw [ne_none_iff_is_some, is_some_iff_exists] at hl,
      cases hl with lmax ismax,
      have := le_maximum_of_mem hb ismax,
      apply' lt_of_le_of_lt this,
      rw ismax at hlo,
      exact with_bot.coe_lt_coe.mp hlo,
   end,
   exact prod_lt_one_lt_one hl this,
end

lemma remove_nth_subset {α : Type*} : ∀ (l : list α) (n : ℕ), l.remove_nth n ⊆ l
| []     n       := by rw remove_nth; exact list.subset.refl nil
| (a::l) 0       := by rw remove_nth; exact list.subset_cons _ _
| (a::l) (n + 1) := by rw [remove_nth, cons_subset, mem_cons_iff]; exact ⟨or.inl rfl, subset_cons_of_subset a (remove_nth_subset l n)⟩

lemma prod_le_one_min_le_one {l : list ℝ≥0} (hl : l ≠ []) (hlo : l.prod ≤ 1) : l.minimum ≤ 1 :=
begin
   contrapose hlo,
   rw not_le at *,
   have : (∀ (a : ℝ≥0) (ha : a ∈ l), 1 < a) :=
   begin
      intros b hb,
      rw [ne.def] at hl,
      rw ← minimum_eq_none at hl,
      change l.minimum ≠ none at hl,
      rw ne_none_iff_is_some at hl,
      rw is_some_iff_exists at hl,
      cases hl with lmin ismin,
      have := minimum_le_of_mem hb ismin,
      convert lt_of_lt_of_le _ this,
      rw ismin at hlo,
      exact with_top.coe_lt_coe.mp hlo,
   end,
   exact prod_gt_one_gt_one hl this,
end

lemma nnreal.mul_div_assoc {a b c : ℝ≥0} : a * b / c = a * (b / c) :=
begin
apply nnreal.eq,
rw [nnreal.coe_div, nnreal.coe_mul],
exact mul_div_assoc _ _ _,
end

lemma nnreal.coe_inj {a b : ℝ≥0} (h : a ≠ b) : (↑ a:ℝ) ≠ b :=
begin
intro hy,
have := nnreal.eq hy,
exact h this,
end

@[simp] lemma nnreal.div_self {a : ℝ≥0} (h : a ≠ 0) : a / a = 1 :=
begin
apply nnreal.eq,
rw [nnreal.coe_div, nnreal.coe_one],
have : (↑a : ℝ) ≠ ↑ 0 := nnreal.coe_inj h,
exact div_self this,
end

lemma nnreal.div_eq_iff {a b c : ℝ≥0} (h : a * b = c) (hh : b ≠ 0) : a = c / b := 
begin
have := congr_arg (λ x, x / b) h,
dsimp at this,
rwa [nnreal.mul_div_assoc, nnreal.div_self hh,mul_one] at this,
end
--set_option profiler true

lemma prod_eq_one_length_le_sum {l : list ℝ≥0} (h : l.prod = 1) : (l.length : ℝ≥0) ≤ l.sum :=
begin
induction hl : l.length generalizing l,
{ simp only [nat.nat_zero_eq_zero, nat.cast_zero], exact zero_le (sum l), },
{

   have : ¬ l = [] := ne_nil_of_length_eq_succ hl,
   rw ← maximum_eq_none at this,
   change l.maximum ≠ none at this,
   rw [ne_none_iff_is_some,is_some_iff_exists] at this,
   cases this with lmax ismax,

   have lmax_mem : lmax ∈ l := maximum_mem ismax,

   have one_le_lmaxim : 1 ≤ l.maximum := prod_ge_one_max_ge_one (ne_nil_of_length_eq_succ hl) (le_of_eq (eq.symm h)),
   obtain ⟨maxind, hmaxind, hmaxeq⟩ := nth_le_of_mem lmax_mem,
   let l' := (l.remove_nth maxind),

   by_cases h_l'_nil : l' = [],
   {
      have n_length_l' : n = length l' :=
      begin
         simp only [l', length],
         rwa [length_remove_nth,hl, nat.succ_sub_succ_eq_sub, nat.sub_zero],
      end,
      rw n_length_l',
      have : length l' = 0 := (congr_arg length h_l'_nil),
      rw this at ⊢ n_length_l',
      have : length l = 1 := by rwa n_length_l' at hl,
      obtain ⟨a, ha⟩ := length_eq_one.mp this,
      rw [ha, sum_cons, sum_nil, add_zero, nat.cast_succ, nat.cast_zero, zero_add],
      rw [ha, prod_cons, prod_nil, mul_one] at h,
      rw h,
   },
   have h_lmin := h_l'_nil,
   rw ← minimum_eq_none at h_lmin,
   change l'.minimum ≠ none at h_lmin,
   rw [ne_none_iff_is_some, is_some_iff_exists] at h_lmin,
   cases h_lmin with lmin ismin,

   have l'min_mem : lmin ∈ l' := minimum_mem ismin,
   have l'_subset_l : l' ⊆ l := remove_nth_subset _ _,
   have lmin_mem : lmin ∈ l := l'_subset_l l'min_mem,

   have l'length : l'.length = l.length - 1 := length_remove_nth l maxind ‹_›,
   let l'' := (l'.update_nth (l'.index_of lmin) (lmax * lmin)),
   have : l''.length = l'.length := update_nth_length _ _ _,
   have l''length : l''.length = n := by rw [this, l'length]; exact nat.pred_eq_of_eq_succ hl,
   have l'prod : l'.prod * lmax = l.prod :=
   begin
      simp only [l'],
      rw [← hmaxeq, prod_remove_nth],
   end,
   have prod_ne_zero : l.prod ≠ 0 :=
   begin
      have := one_ne_zero,
      rwa ← h at this,
   end,

   have lmin_ne_zero : lmin ≠ 0 := prod_ne_zero_elem_ne_zero prod_ne_zero lmin_mem,
   have l''prod : l'.prod * (lmax * lmin) = l''.prod * lmin := begin
      have := prod_update_nth l' (l'.index_of lmin) (index_of_lt_length.mpr l'min_mem) (lmax * lmin),
      simp only [index_of_nth_le, length, nth_le] at this,
      rw ← this,
   end,
   have : l''.prod = l.prod :=
   begin
      rw ← nnreal.mul_eq_mul_left lmin_ne_zero, -- TODO mul_right version
      conv_lhs { rw mul_comm, },
      conv_rhs { rw mul_comm, },
      rw [← l''prod,  ← mul_assoc,  l'prod],
   end,
   have h2 := h,
   rw ← this at h2,
   have one_le_lmax := ((with_bot.coe_le ismax).mp one_le_lmaxim),
   have n_le_sum_l'' := ih h2 l''length,
   have lmax_ne_zero : lmax ≠ 0 := prod_ne_zero_elem_ne_zero prod_ne_zero lmax_mem,
   have : l'.prod ≤ 1 :=
   begin
      simp only [l'],

      have := prod_remove_nth l maxind hmaxind,
      rw [hmaxeq, h] at this,
      have : prod (remove_nth l maxind) = 1 / lmax := nnreal.div_eq_iff this lmax_ne_zero,
      rw [this, ← nnreal.coe_le, nnreal.coe_div, nnreal.coe_one, one_div_eq_inv],
      exact inv_le_one one_le_lmax,
   end,
   have := prod_le_one_min_le_one h_l'_nil this,
   have lmin_le_one := ((with_top.le_coe ismin).mp this),
   have := aux one_le_lmax lmin_le_one,
   have : ↑n + 1 ≤ sum l'' + (lmax + lmin - lmax * lmin) := add_le_add n_le_sum_l'' this,
   convert this,
   simp only [l''],
   apply nnreal.eq,
   rw [nnreal.coe_add, nnreal.coe_sub],
   { 
      simp only [add_comm, nnreal.coe_add, sub_eq_add_neg, nnreal.coe_mul],
      have := nnreal.eq_iff.mpr (sum_update_nth l' (l'.index_of lmin) (index_of_lt_length.mpr l'min_mem) (lmax * lmin)),
      simp only [index_of_nth_le, length, nnreal.coe_add, nth_le, nnreal.coe_mul] at this,
      conv_rhs{ congr,skip,congr, rw add_comm,},
      conv_rhs{ rw [← add_assoc, ← add_assoc, this],},
      simp only [l', add_zero, add_comm, add_left_neg, add_left_comm],
      have := sum_remove_nth l maxind hmaxind,
      rw hmaxeq at this,
      rw [← this],
      simp only [add_comm, nnreal.coe_add, zero_add, add_right_inj],
   },
   rw [ ← nnreal.coe_le, nnreal.coe_add, nnreal.coe_mul],
   have lmin_nonneg : 0 ≤ (↑lmin:ℝ):= lmin.2,
   have lmax_nonneg : 0 ≤ (↑lmax:ℝ):= lmax.2,
   have lmax_pos : 0 < (↑lmax:ℝ) := lt_of_le_of_ne lmax_nonneg (begin rw ← nnreal.coe_zero, apply nnreal.coe_inj, intro fh, rw ← fh at one_le_lmax, simpa using one_le_lmax, end),
   transitivity ↑lmax,
   {
      have : (↑lmin:ℝ) ≤ 1 := lmin_le_one,
      suffices : ↑lmax * ↑lmin ≤ ↑lmax * (1 : ℝ), by simpa using this,
      exact (mul_le_mul_left lmax_pos).mpr lmin_le_one,
   },
   {
      convert add_le_add_left lmin_nonneg (↑lmax),
      simp only [add_zero],
   }
},
end

noncomputable instance nnreal_has_rpow : has_pow ℝ≥0 ℝ := ⟨λ x y, ⟨x^y, real.rpow_nonneg_of_nonneg x.2 y⟩⟩ 

lemma rpow_mul {x : ℝ≥0} (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z :=
begin dsimp [nnreal_has_rpow], apply nnreal.eq, rw subtype.coe_mk, rw subtype.coe_mk, rw ← real.rpow_mul, exact zero_le x, end

@[simp] lemma rpow_one {x : ℝ≥0} : x ^ (1 : ℝ) = x :=
begin dsimp [nnreal_has_rpow], apply nnreal.eq, rw subtype.coe_mk, rw real.rpow_one, end
@[simp] lemma zero_rpow {x : ℝ} (h : x ≠ 0) : (0 : ℝ≥0)^x = 0 :=
begin dsimp [nnreal_has_rpow], apply nnreal.eq, rw subtype.coe_mk, rw real.zero_rpow, simpa, end

lemma nnreal.rpow_mul_nat {x : ℝ≥0} (y : ℝ) (z : ℕ) : x ^ (y * z) = (x ^ y) ^ z :=
begin
rw rpow_mul,
dsimp [nnreal_has_rpow],
apply nnreal.eq,
rw [coe_pow, subtype.coe_mk, real.rpow_nat_cast, subtype.coe_mk],
end

lemma nnreal.rpow_neg {x : ℝ≥0} (y : ℝ) : x ^ -y = (x ^ y)⁻¹ :=
begin
dsimp [nnreal_has_rpow],
apply nnreal.eq,
rw [subtype.coe_mk],
exact real.rpow_neg (coe_nonneg x) y,
end

@[simp] lemma nnreal.rpow_nat_cast {x : ℝ≥0} (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
begin
dsimp [nnreal_has_rpow],
apply nnreal.eq,
rw [subtype.coe_mk, real.rpow_nat_cast],
symmetry,
exact coe_pow _ _,
end


@[simp] lemma nnreal.pow_nat_rpow_nat_inv {x : ℝ≥0} {n : ℕ} (hn : 0 < n) :
  (x ^ n) ^ (n⁻¹ : ℝ) = x :=
begin
dsimp [nnreal_has_rpow],
apply nnreal.eq,
rw [subtype.coe_mk, coe_pow],
exact real.pow_nat_rpow_nat_inv (coe_nonneg x) hn,
end

--TODO @[simp] lemma rpow_int_cast (x : ℝ≥0) (n : ℤ) : x ^ (n : ℝ) = x ^ n :=

instance (g : ℝ≥0) : is_add_monoid_hom ((*) g) := { map_add := mul_add g,
  map_zero := mul_zero g }


@[to_additive]
theorem is_monoid_hom.map_prod {α β : Type*} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] (l : list α) :
  f (prod l) = prod (map f l) :=
by induction l; simp only [*, is_mul_hom.map_mul f, is_monoid_hom.map_one f, prod_nil, prod_cons, map]

lemma muow_length {g : ℝ≥0} {l : list ℝ≥0} : (l.map ((*) g)).sum = (*) g l.sum:=
 eq.symm (is_add_monoid_hom.map_sum ((*) g) l)

lemma mul_prod_pow_length {g : ℝ≥0} {l : list ℝ≥0} : (l.map ((*) g)).prod = l.prod * g ^ l.length :=
begin
induction l,
{
   simp only [mul_one, list.length, list.prod_nil, pow_zero, list.map],
},
{
   simp only [l_ih, add_comm, map, length, prod_cons],
   conv_lhs{congr, rw mul_comm},
   rw mul_assoc,
   rw mul_assoc,
   conv_lhs
   {congr,skip,rw← mul_assoc,congr,rw mul_comm,},
   rw mul_assoc,
   rw pow_add,
   rw pow_one,
}
end

lemma amgm {l : list ℝ≥0} : (l.prod)^(1 / (l.length : ℝ)) * l.length ≤ l.sum :=
begin
   by_cases hl : l.length = 0,
   {
      simp only [hl, div_zero, nat.cast_zero, list.length, mul_zero],
      exact zero_le _,
   },
   set g := (l.prod)^(1 / (l.length : ℝ)),
   by_cases h : g = 0,
   {
      rw h,
      simp only [zero_mul, list.length],
      exact zero_le _,
   },
   {
      rw ← ne.def at h,
      have gpos : 0 < g := zero_lt_iff_ne_zero.mpr h,
      have : l.prod ≠ 0 :=
      begin
         intro hh, simp only [g, one_div_eq_inv, length, ne.def, hh] at h, 
         apply h,
         apply' zero_rpow, apply inv_ne_zero, exact_mod_cast hl,
      end,
      set divg := ((*) (g ^ (-1 : ℝ))),
      haveI divg_gp_hom : is_add_monoid_hom divg := by apply_instance,
      have : (l.map divg).prod = 1 := begin
         have : (l.map divg).prod = l.prod * (g ^ (-1 : ℝ))^ l.length := mul_prod_pow_length,
         simp only [g, one_div_eq_inv, map, length, one_div_eq_inv, map, length] at this,
         rw [← nnreal.rpow_mul_nat] at this,
         rw this,
         simp only [neg_mul_eq_neg_mul_symm, one_mul, length],
         rw [← rpow_mul],
         simp only [length, mul_neg_eq_neg_mul_symm],
         rw field.inv_mul_cancel,
         have : (prod l)^(-1: ℝ) = (prod l)⁻¹ := by rw [nnreal.rpow_neg, rpow_one],
         rw this,
         rwa nnreal.mul_inv_cancel,
         exact_mod_cast hl,
      end,
      have ineq := prod_eq_one_length_le_sum this,
      simp only [map, length, length_map] at ineq,
      have : divg l.sum = (map divg l).sum :=
      is_add_monoid_hom.map_sum _ _,
      rw ← this at ineq,
      dsimp [divg] at ineq,
      rw [nnreal.rpow_neg, rpow_one] at ineq,
      rwa mul_le_iff_le_inv h,
   }
end


#lint