/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Johannes Hölzl, Mario Carneiro

Cardinal arithmetic.

Cardinals are represented as quotient over equinumerous types.
-/

import data.set.finite data.quot logic.function set_theory.schroeder_bernstein

open function lattice set
local attribute [instance] classical.prop_decidable

universes u v w x

instance cardinal.is_equivalent : setoid (Type u) :=
{ r := λα β, nonempty (α ≃ β),
  iseqv := ⟨λα,
    ⟨equiv.refl α⟩,
    λα β ⟨e⟩, ⟨e.symm⟩,
    λα β γ ⟨e₁⟩ ⟨e₂⟩, ⟨e₁.trans e₂⟩⟩ }

/-- `cardinal.{u}` is the type of cardinal numbers in `Type u`,
  defined as the quotient of `Type u` by existence of an equivalence
  (a bijection with explicit inverse). -/
def cardinal : Type (u + 1) := quotient cardinal.is_equivalent

namespace cardinal

/-- The cardinal of a type -/
def mk : Type u → cardinal := quotient.mk

@[simp] theorem mk_def (α : Type u) : @eq cardinal ⟦α⟧ (mk α) := rfl

@[simp] theorem mk_out (c : cardinal) : mk (c.out) = c := quotient.out_eq _

instance : has_le cardinal.{u} :=
⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, nonempty $ α ↪ β) $
  assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
    propext ⟨assume ⟨e⟩, ⟨e.congr e₁ e₂⟩, assume ⟨e⟩, ⟨e.congr e₁.symm e₂.symm⟩⟩⟩

theorem mk_le_of_injective {α β : Type u} {f : α → β} (hf : injective f) : mk α ≤ mk β :=
⟨⟨f, hf⟩⟩

theorem mk_le_of_surjective {α β : Type u} {f : α → β} (hf : surjective f) : mk β ≤ mk α :=
⟨embedding.of_surjective hf⟩

theorem le_mk_iff_exists_set {c : cardinal} {α : Type u} :
  c ≤ mk α ↔ ∃ p : set α, mk p = c :=
⟨quotient.induction_on c $ λ β ⟨⟨f, hf⟩⟩,
  ⟨set.range f, eq.symm $ quot.sound ⟨equiv.set.range f hf⟩⟩,
λ ⟨p, e⟩, e ▸ ⟨⟨subtype.val, λ a b, subtype.eq⟩⟩⟩

instance : linear_order cardinal.{u} :=
{ le          := (≤),
  le_refl     := by rintros ⟨α⟩; exact ⟨embedding.refl _⟩,
  le_trans    := by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.trans e₂⟩,
  le_antisymm := by rintros ⟨α⟩ ⟨β⟩ ⟨e₁⟩ ⟨e₂⟩; exact quotient.sound (e₁.antisymm e₂),
  le_total    := by rintros ⟨α⟩ ⟨β⟩; exact embedding.total }

noncomputable instance : decidable_linear_order cardinal.{u} := classical.DLO _

noncomputable instance : distrib_lattice cardinal.{u} := by apply_instance

instance : has_zero cardinal.{u} := ⟨⟦pempty⟧⟩

instance : inhabited cardinal.{u} := ⟨0⟩

theorem ne_zero_iff_nonempty {α : Type u} : mk α ≠ 0 ↔ nonempty α :=
not_iff_comm.1
  ⟨λ h, quotient.sound ⟨(equiv.empty_of_not_nonempty h).trans equiv.empty_equiv_pempty⟩,
   λ e, let ⟨h⟩ := quotient.exact e in λ ⟨a⟩, (h a).elim⟩

instance : has_one cardinal.{u} := ⟨⟦punit⟧⟩

instance : zero_ne_one_class cardinal.{u} :=
{ zero := 0, one := 1, zero_ne_one :=
  ne.symm $ ne_zero_iff_nonempty.2 ⟨punit.star⟩ }

theorem le_one_iff_subsingleton {α : Type u} : mk α ≤ 1 ↔ subsingleton α :=
⟨λ ⟨f⟩, ⟨λ a b, f.inj (subsingleton.elim _ _)⟩,
 λ ⟨h⟩, ⟨⟨λ a, punit.star, λ a b _, h _ _⟩⟩⟩

instance : has_add cardinal.{u} :=
⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, mk (α ⊕ β)) $ assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
  quotient.sound ⟨equiv.sum_congr e₁ e₂⟩⟩

@[simp] theorem add_def (α β) : mk α + mk β = mk (α ⊕ β) := rfl

instance : has_mul cardinal.{u} :=
⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, mk (α × β)) $ assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
  quotient.sound ⟨equiv.prod_congr e₁ e₂⟩⟩

@[simp] theorem mul_def (α β) : mk α * mk β = mk (α × β) := rfl

private theorem add_comm (a b : cardinal.{u}) : a + b = b + a :=
quotient.induction_on₂ a b $ assume α β, quotient.sound ⟨equiv.sum_comm α β⟩

private theorem mul_comm (a b : cardinal.{u}) : a * b = b * a :=
quotient.induction_on₂ a b $ assume α β, quotient.sound ⟨equiv.prod_comm α β⟩

private theorem zero_add (a : cardinal.{u}) : 0 + a = a :=
quotient.induction_on a $ assume α, quotient.sound ⟨equiv.pempty_sum α⟩

private theorem zero_mul (a : cardinal.{u}) : 0 * a = 0 :=
quotient.induction_on a $ assume α, quotient.sound ⟨equiv.pempty_prod α⟩

private theorem one_mul (a : cardinal.{u}) : 1 * a = a :=
quotient.induction_on a $ assume α, quotient.sound ⟨equiv.punit_prod α⟩

private theorem left_distrib (a b c : cardinal.{u}) : a * (b + c) = a * b + a * c :=
quotient.induction_on₃ a b c $ assume α β γ, quotient.sound ⟨equiv.prod_sum_distrib α β γ⟩

instance : comm_semiring cardinal.{u} :=
{ zero          := 0,
  one           := 1,
  add           := (+),
  mul           := (*),
  zero_add      := zero_add,
  add_zero      := assume a, by rw [add_comm a 0, zero_add a],
  add_assoc     := λa b c, quotient.induction_on₃ a b c $ assume α β γ,
    quotient.sound ⟨equiv.sum_assoc α β γ⟩,
  add_comm      := add_comm,
  zero_mul      := zero_mul,
  mul_zero      := assume a, by rw [mul_comm a 0, zero_mul a],
  one_mul       := one_mul,
  mul_one       := assume a, by rw [mul_comm a 1, one_mul a],
  mul_assoc     := λa b c, quotient.induction_on₃ a b c $ assume α β γ,
    quotient.sound ⟨equiv.prod_assoc α β γ⟩,
  mul_comm      := mul_comm,
  left_distrib  := left_distrib,
  right_distrib := assume a b c,
    by rw [mul_comm (a + b) c, left_distrib c a b, mul_comm c a, mul_comm c b] }

/-- The cardinal exponential. `mk α ^ mk β` is the cardinal of `β → α`. -/
protected def power (a b : cardinal.{u}) : cardinal.{u} :=
quotient.lift_on₂ a b (λα β, mk (β → α)) $ assume α₁ α₂ β₁ β₂ ⟨e₁⟩ ⟨e₂⟩,
  quotient.sound ⟨equiv.arrow_congr e₂ e₁⟩

instance : has_pow cardinal cardinal := ⟨cardinal.power⟩
local infixr ^ := @has_pow.pow cardinal cardinal cardinal.has_pow

@[simp] theorem power_def (α β) : mk α ^ mk β = mk (β → α) := rfl

@[simp] theorem power_zero {a : cardinal} : a ^ 0 = 1 :=
quotient.induction_on a $ assume α, quotient.sound
⟨equiv.pempty_arrow_equiv_punit α⟩

@[simp] theorem power_one {a : cardinal} : a ^ 1 = a :=
quotient.induction_on a $ assume α, quotient.sound
⟨equiv.punit_arrow_equiv α⟩

@[simp] theorem one_power {a : cardinal} : 1 ^ a = 1 :=
quotient.induction_on a $ assume α, quotient.sound
⟨equiv.arrow_punit_equiv_punit α⟩

@[simp] theorem prop_eq_two : mk (ulift Prop) = 2 :=
quot.sound ⟨equiv.ulift.trans $ equiv.Prop_equiv_bool.trans equiv.bool_equiv_punit_sum_punit⟩

@[simp] theorem zero_power {a : cardinal} : a ≠ 0 → 0 ^ a = 0 :=
quotient.induction_on a $ assume α heq,
nonempty.rec_on (ne_zero_iff_nonempty.1 heq) $ assume a,
quotient.sound ⟨equiv.equiv_pempty $ assume f, pempty.rec (λ _, false) (f a)⟩

theorem power_ne_zero {a : cardinal} (b) : a ≠ 0 → a ^ b ≠ 0 :=
quotient.induction_on₂ a b $ λ α β h,
let ⟨a⟩ := ne_zero_iff_nonempty.1 h in
ne_zero_iff_nonempty.2 ⟨λ _, a⟩

theorem mul_power {a b c : cardinal} : (a * b) ^ c = a ^ c * b ^ c :=
quotient.induction_on₃ a b c $ assume α β γ,
  quotient.sound ⟨equiv.arrow_prod_equiv_prod_arrow α β γ⟩

theorem power_add {a b c : cardinal} : a ^ (b + c) = a ^ b * a ^ c :=
quotient.induction_on₃ a b c $ assume α β γ,
  quotient.sound ⟨equiv.sum_arrow_equiv_prod_arrow β γ α⟩

theorem power_mul {a b c : cardinal} : (a ^ b) ^ c = a ^ (b * c) :=
by rw [_root_.mul_comm b c];
from (quotient.induction_on₃ a b c $ assume α β γ,
  quotient.sound ⟨equiv.arrow_arrow_equiv_prod_arrow γ β α⟩)

section order_properties
open sum

theorem zero_le : ∀(a : cardinal), 0 ≤ a :=
by rintro ⟨α⟩; exact ⟨embedding.of_not_nonempty $ λ ⟨a⟩, a.elim⟩

theorem le_zero (a : cardinal) : a ≤ 0 ↔ a = 0 :=
by simp [le_antisymm_iff, zero_le]

theorem pos_iff_ne_zero {o : cardinal} : 0 < o ↔ o ≠ 0 :=
by simp [lt_iff_le_and_ne, eq_comm, zero_le]

theorem zero_lt_one : (0 : cardinal) < 1 :=
lt_of_le_of_ne (zero_le _) zero_ne_one

theorem add_le_add : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d :=
by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨embedding.sum_congr e₁ e₂⟩

theorem add_le_add_left (a) {b c : cardinal} : b ≤ c → a + b ≤ a + c :=
add_le_add (le_refl _)

theorem add_le_add_right {a b : cardinal} (c) (h : a ≤ b) : a + c ≤ b + c :=
add_le_add h (le_refl _)

theorem le_add_right (a b : cardinal) : a ≤ a + b :=
by simpa using add_le_add_left a (zero_le b)

theorem le_add_left (a b : cardinal) : a ≤ b + a :=
by simpa using add_le_add_right a (zero_le b)

theorem mul_le_mul : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a * c ≤ b * d :=
by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨embedding.prod_congr e₁ e₂⟩

theorem mul_le_mul_left (a) {b c : cardinal} : b ≤ c → a * b ≤ a * c :=
mul_le_mul (le_refl _)

theorem mul_le_mul_right {a b : cardinal} (c) (h : a ≤ b) : a * c ≤ b * c :=
mul_le_mul h (le_refl _)

theorem power_le_power_left : ∀{a b c : cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=
by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩; exact
  let ⟨a⟩ := ne_zero_iff_nonempty.1 hα in
  ⟨@embedding.arrow_congr_right _ _ _ ⟨a⟩ e⟩

theorem power_le_power_right {a b c : cardinal} : a ≤ b → a ^ c ≤ b ^ c :=
quotient.induction_on₃ a b c $ assume α β γ ⟨e⟩, ⟨embedding.arrow_congr_left e⟩

theorem le_iff_exists_add {a b : cardinal} : a ≤ b ↔ ∃ c, b = a + c :=
⟨quotient.induction_on₂ a b $ λ α β ⟨⟨f, hf⟩⟩,
  have (α ⊕ ↥-range f) ≃ β, from
    (equiv.sum_congr (equiv.set.range f hf) (equiv.refl _)).trans $
    (equiv.set.sum_compl (range f)),
  ⟨⟦(-range f : set β)⟧, quotient.sound ⟨this.symm⟩⟩,
 λ ⟨c, e⟩, add_zero a ▸ e.symm ▸ add_le_add_left _ (zero_le _)⟩

end order_properties

instance : order_bot cardinal.{u} :=
{ bot := 0, bot_le := zero_le, ..cardinal.linear_order }

instance : canonically_ordered_monoid cardinal.{u} :=
{ add_le_add_left       := λ a b h c, add_le_add_left _ h,
  lt_of_add_lt_add_left := λ a b c, lt_imp_lt_of_le_imp_le (add_le_add_left _),
  le_iff_exists_add     := @le_iff_exists_add,
  ..cardinal.lattice.order_bot,
  ..cardinal.comm_semiring, ..cardinal.linear_order }

theorem cantor : ∀(a : cardinal.{u}), a < 2 ^ a :=
by rw ← prop_eq_two; rintros ⟨a⟩; exact ⟨
  ⟨⟨λ a b, ⟨a = b⟩, λ a b h, cast (ulift.up.inj (@congr_fun _ _ _ _ h b)).symm rfl⟩⟩,
  λ ⟨⟨f, hf⟩⟩, cantor_injective (λ s, f (λ a, ⟨s a⟩)) $
    λ s t h, by funext a; injection congr_fun (hf h) a⟩

instance : no_top_order cardinal.{u} :=
{ no_top := λ a, ⟨_, cantor a⟩, ..cardinal.linear_order }

/-- The minimum cardinal in a family of cardinals (the existence
  of which is provided by `injective_min`). -/
noncomputable def min {ι} (I : nonempty ι) (f : ι → cardinal) : cardinal :=
f $ classical.some $
@embedding.injective_min _ (λ i, (f i).out) I

theorem min_eq {ι} (I) (f : ι → cardinal) : ∃ i, min I f = f i :=
⟨_, rfl⟩

theorem min_le {ι I} (f : ι → cardinal) (i) : min I f ≤ f i :=
by rw [← mk_out (min I f), ← mk_out (f i)]; exact
let ⟨g⟩ := classical.some_spec
  (@embedding.injective_min _ (λ i, (f i).out) I) in
⟨g i⟩

theorem le_min {ι I} {f : ι → cardinal} {a} : a ≤ min I f ↔ ∀ i, a ≤ f i :=
⟨λ h i, le_trans h (min_le _ _),
 λ h, let ⟨i, e⟩ := min_eq I f in e.symm ▸ h i⟩

protected theorem wf : @well_founded cardinal.{u} (<) :=
⟨λ a, classical.by_contradiction $ λ h,
  let ι := {c :cardinal // ¬ acc (<) c},
      f : ι → cardinal := subtype.val,
      ⟨⟨c, hc⟩, hi⟩ := @min_eq ι ⟨⟨_, h⟩⟩ f in
    hc (acc.intro _ (λ j ⟨_, h'⟩,
      classical.by_contradiction $ λ hj, h' $
      by have := min_le f ⟨j, hj⟩; rwa hi at this))⟩

instance has_wf : @has_well_founded cardinal.{u} := ⟨(<), cardinal.wf⟩

instance wo : @is_well_order cardinal.{u} (<) := ⟨cardinal.wf⟩

/-- The successor cardinal - the smallest cardinal greater than
  `c`. This is not the same as `c + 1` except in the case of finite `c`. -/
noncomputable def succ (c : cardinal) : cardinal :=
@min {c' // c < c'} ⟨⟨_, cantor _⟩⟩ subtype.val

theorem lt_succ_self (c : cardinal) : c < succ c :=
by cases min_eq _ _ with s e; rw [succ, e]; exact s.2

theorem succ_le {a b : cardinal} : succ a ≤ b ↔ a < b :=
⟨lt_of_lt_of_le (lt_succ_self _), λ h,
  by exact min_le _ (subtype.mk b h)⟩

theorem lt_succ {a b : cardinal} : a < succ b ↔ a ≤ b :=
by rw [← not_le, succ_le, not_lt]

theorem add_one_le_succ (c : cardinal) : c + 1 ≤ succ c :=
begin
  refine quot.induction_on c (λ α, _) (lt_succ_self c),
  refine quot.induction_on (succ (quot.mk setoid.r α)) (λ β h, _),
  cases h.left with f,
  have : ¬ surjective f := λ hn,
    ne_of_lt h (quotient.sound ⟨equiv.of_bijective ⟨f.inj, hn⟩⟩),
  cases classical.not_forall.1 this with b nex,
  refine ⟨⟨sum.rec (by exact f) _, _⟩⟩,
  { exact λ _, b },
  { intros a b h, rcases a with a|⟨⟨⟨⟩⟩⟩; rcases b with b|⟨⟨⟨⟩⟩⟩,
    { rw f.inj h },
    { exact nex.elim ⟨_, h⟩ },
    { exact nex.elim ⟨_, h.symm⟩ },
    { refl } }
end

/-- The indexed sum of cardinals is the cardinality of the
  indexed disjoint union, i.e. sigma type. -/
def sum {ι} (f : ι → cardinal) : cardinal := mk Σ i, (f i).out

theorem le_sum {ι} (f : ι → cardinal) (i) : f i ≤ sum f :=
by rw ← quotient.out_eq (f i); exact
⟨⟨λ a, ⟨i, a⟩, λ a b h, eq_of_heq $ by injection h⟩⟩

@[simp] theorem sum_mk {ι} (f : ι → Type*) : sum (λ i, mk (f i)) = mk (Σ i, f i) :=
quot.sound ⟨equiv.sigma_congr_right $ λ i,
  classical.choice $ quotient.exact $ quot.out_eq $ mk (f i)⟩

theorem sum_const (ι : Type u) (a : cardinal.{u}) : sum (λ _:ι, a) = mk ι * a :=
quotient.induction_on a $ λ α, by simp; exact
  quotient.sound ⟨equiv.sigma_equiv_prod _ _⟩

theorem sum_le_sum {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=
⟨embedding.sigma_congr_right $ λ i, classical.choice $
  by have := H i; rwa [← quot.out_eq (f i), ← quot.out_eq (g i)] at this⟩

/-- The indexed supremum of cardinals is the smallest cardinal above
  everything in the family. -/
noncomputable def sup {ι} (f : ι → cardinal) : cardinal :=
@min {c // ∀ i, f i ≤ c} ⟨⟨sum f, le_sum f⟩⟩ (λ a, a.1)

theorem le_sup {ι} (f : ι → cardinal) (i) : f i ≤ sup f :=
by dsimp [sup]; cases min_eq _ _ with c hc; rw hc; exact c.2 i

theorem sup_le {ι} {f : ι → cardinal} {a} : sup f ≤ a ↔ ∀ i, f i ≤ a :=
⟨λ h i, le_trans (le_sup _ _) h,
 λ h, by dsimp [sup]; change a with (⟨a, h⟩:subtype _).1; apply min_le⟩

theorem sup_le_sup {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sup f ≤ sup g :=
sup_le.2 $ λ i, le_trans (H i) (le_sup _ _)

theorem sup_le_sum {ι} (f : ι → cardinal) : sup f ≤ sum f :=
sup_le.2 $ le_sum _

theorem sum_le_sup {ι : Type u} (f : ι → cardinal.{u}) : sum f ≤ mk ι * sup.{u u} f :=
by rw ← sum_const; exact sum_le_sum _ _ (le_sup _)

/-- The indexed product of cardinals is the cardinality of the Pi type
  (dependent product). -/
def prod {ι : Type u} (f : ι → cardinal) : cardinal := mk (Π i, (f i).out)

@[simp] theorem prod_mk {ι} (f : ι → Type*) : prod (λ i, mk (f i)) = mk (Π i, f i) :=
quot.sound ⟨equiv.Pi_congr_right $ λ i,
  classical.choice $ quotient.exact $ mk_out $ mk (f i)⟩

theorem prod_const (ι : Type u) (a : cardinal.{u}) : prod (λ _:ι, a) = a ^ mk ι :=
quotient.induction_on a $ by simp

theorem prod_le_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : prod f ≤ prod g :=
⟨embedding.Pi_congr_right $ λ i, classical.choice $
  by have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this⟩

theorem prod_ne_zero {ι} (f : ι → cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0 :=
begin
  conv in (f _) {rw ← mk_out (f i)},
  simp [prod, ne_zero_iff_nonempty, -mk_out, -ne.def],
  exact ⟨λ ⟨F⟩ i, ⟨F i⟩, λ h, ⟨λ i, classical.choice (h i)⟩⟩,
end

theorem prod_eq_zero {ι} (f : ι → cardinal) : prod f = 0 ↔ ∃ i, f i = 0 :=
not_iff_not.1 $ by simpa using prod_ne_zero f

/-- The universe lift operation on cardinals -/
def lift (c : cardinal.{u}) : cardinal.{max u v} :=
quotient.lift_on c (λ α, ⟦ulift α⟧) $ λ α β ⟨e⟩,
quotient.sound ⟨equiv.ulift.trans $ e.trans equiv.ulift.symm⟩

theorem lift_mk (α) : lift.{u v} (mk α) = mk (ulift.{v u} α) := rfl

theorem lift_umax : lift.{u (max u v)} = lift.{u v} :=
funext $ λ a, quot.induction_on a $ λ α,
quotient.sound ⟨equiv.ulift.trans equiv.ulift.symm⟩

theorem lift_id' (a : cardinal) : lift a = a :=
quot.induction_on a $ λ α, quot.sound ⟨equiv.ulift⟩

@[simp] theorem lift_id : ∀ a, lift.{u u} a = a := lift_id'.{u u}

@[simp] theorem lift_lift (a : cardinal) : lift.{(max u v) w} (lift.{u v} a) = lift.{u (max v w)} a :=
quot.induction_on a $ λ α,
quotient.sound ⟨equiv.ulift.trans $ equiv.ulift.trans equiv.ulift.symm⟩

theorem lift_mk_le {α : Type u} {β : Type v} :
  lift.{u (max v w)} (mk α) ≤ lift.{v (max u w)} (mk β) ↔ nonempty (α ↪ β) :=
⟨λ ⟨f⟩, ⟨embedding.congr equiv.ulift equiv.ulift f⟩,
 λ ⟨f⟩, ⟨embedding.congr equiv.ulift.symm equiv.ulift.symm f⟩⟩

theorem lift_mk_eq {α : Type u} {β : Type v} :
  lift.{u (max v w)} (mk α) = lift.{v (max u w)} (mk β) ↔ nonempty (α ≃ β) :=
quotient.eq.trans
⟨λ ⟨f⟩, ⟨equiv.ulift.symm.trans $ f.trans equiv.ulift⟩,
 λ ⟨f⟩, ⟨equiv.ulift.trans $ f.trans equiv.ulift.symm⟩⟩

@[simp] theorem lift_le {a b : cardinal} : lift a ≤ lift b ↔ a ≤ b :=
quotient.induction_on₂ a b $ λ α β,
by rw ← lift_umax; exact lift_mk_le

@[simp] theorem lift_inj {a b : cardinal} : lift a = lift b ↔ a = b :=
by simp [le_antisymm_iff]

@[simp] theorem lift_lt {a b : cardinal} : lift a < lift b ↔ a < b :=
by simp [lt_iff_le_not_le, -not_le]

@[simp] theorem lift_zero : lift 0 = 0 :=
quotient.sound ⟨equiv.ulift.trans equiv.pempty_equiv_pempty⟩

@[simp] theorem lift_one : lift 1 = 1 :=
quotient.sound ⟨equiv.ulift.trans equiv.punit_equiv_punit⟩

@[simp] theorem lift_add (a b) : lift (a + b) = lift a + lift b :=
quotient.induction_on₂ a b $ λ α β,
quotient.sound ⟨equiv.ulift.trans (equiv.sum_congr equiv.ulift equiv.ulift).symm⟩

@[simp] theorem lift_mul (a b) : lift (a * b) = lift a * lift b :=
quotient.induction_on₂ a b $ λ α β,
quotient.sound ⟨equiv.ulift.trans (equiv.prod_congr equiv.ulift equiv.ulift).symm⟩

@[simp] theorem lift_power (a b) : lift (a ^ b) = lift a ^ lift b :=
quotient.induction_on₂ a b $ λ α β,
quotient.sound ⟨equiv.ulift.trans (equiv.arrow_congr equiv.ulift equiv.ulift).symm⟩

@[simp] theorem lift_two_power (a) : lift (2 ^ a) = 2 ^ lift a :=
by simp [bit0]

@[simp] theorem lift_min {ι I} (f : ι → cardinal) : lift (min I f) = min I (lift ∘ f) :=
le_antisymm (le_min.2 $ λ a, lift_le.2 $ min_le _ a) $
let ⟨i, e⟩ := min_eq I (lift ∘ f) in
by rw e; exact lift_le.2 (le_min.2 $ λ j, lift_le.1 $
by have := min_le (lift ∘ f) j; rwa e at this)

theorem lift_down {a : cardinal.{u}} {b : cardinal.{max u v}} :
  b ≤ lift a → ∃ a', lift a' = b :=
quotient.induction_on₂ a b $ λ α β,
by dsimp; rw [← lift_id (mk β), ← lift_umax, ← lift_umax.{u v}, lift_mk_le]; exact
λ ⟨f⟩, ⟨mk (set.range f), eq.symm $ lift_mk_eq.2
  ⟨embedding.equiv_of_surjective
    (embedding.cod_restrict _ f set.mem_range_self)
    $ λ ⟨a, ⟨b, e⟩⟩, ⟨b, subtype.eq e⟩⟩⟩

theorem le_lift_iff {a : cardinal.{u}} {b : cardinal.{max u v}} :
  b ≤ lift a ↔ ∃ a', lift a' = b ∧ a' ≤ a :=
⟨λ h, let ⟨a', e⟩ := lift_down h in ⟨a', e, lift_le.1 $ e.symm ▸ h⟩,
 λ ⟨a', e, h⟩, e ▸ lift_le.2 h⟩

theorem lt_lift_iff {a : cardinal.{u}} {b : cardinal.{max u v}} :
  b < lift a ↔ ∃ a', lift a' = b ∧ a' < a :=
⟨λ h, let ⟨a', e⟩ := lift_down (le_of_lt h) in
      ⟨a', e, lift_lt.1 $ e.symm ▸ h⟩,
 λ ⟨a', e, h⟩, e ▸ lift_lt.2 h⟩

@[simp] theorem lift_succ (a) : lift (succ a) = succ (lift a) :=
le_antisymm
  (le_of_not_gt $ λ h, begin
    rcases lt_lift_iff.1 h with ⟨b, e, h⟩,
    rw [lt_succ, ← lift_le, e] at h,
    exact not_lt_of_le h (lt_succ_self _)
  end)
  (succ_le.2 $ lift_lt.2 $ lt_succ_self _)

/-- `ω` is the smallest infinite cardinal, also known as ℵ₀. -/
def omega : cardinal.{u} := lift (mk ℕ)

theorem omega_ne_zero : omega ≠ 0 :=
ne_zero_iff_nonempty.2 ⟨⟨0⟩⟩

theorem omega_pos : 0 < omega :=
pos_iff_ne_zero.2 omega_ne_zero

@[simp] theorem lift_omega : lift omega = omega := lift_lift _

@[simp] theorem mk_fin : ∀ (n : ℕ), mk (fin n) = n
| 0     := quotient.sound ⟨(equiv.pempty_of_not_nonempty $ λ ⟨h⟩, h.elim0)⟩
| (n+1) := by rw [nat.cast_succ, ← mk_fin]; exact
  quotient.sound (fintype.card_eq.1 $ by simp)

@[simp] theorem lift_nat_cast (n : ℕ) : lift n = n :=
by induction n; simp *

theorem lift_mk_fin (n : ℕ) : lift (mk (fin n)) = n := by simp

theorem fintype_card (α : Type u) [fintype α] : mk α = fintype.card α :=
by rw [← lift_mk_fin.{u}, ← lift_id (mk α), lift_mk_eq.{u 0 u}];
   exact fintype.card_eq.1 (by simp)

theorem card_le_of_finset {α} (s : finset α) :
  (s.card : cardinal) ≤ cardinal.mk α :=
begin
  rw (_ : (s.card : cardinal) = cardinal.mk (↑s : set α)),
  { exact ⟨function.embedding.subtype _⟩ },
  rw [cardinal.fintype_card, fintype.card_coe]
end

@[simp] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
by induction n; simp [nat.pow_succ, -_root_.add_comm, power_add, *]

@[simp] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
by rw [← lift_mk_fin, ← lift_mk_fin, lift_le]; exact
⟨λ ⟨⟨f, hf⟩⟩, begin
  have : _ = fintype.card _ := finset.card_image_of_injective finset.univ hf,
  simp at this,
  rw [← fintype.card_fin n, ← this],
  exact finset.card_le_of_subset (finset.subset_univ _)
end,
λ h, ⟨⟨λ i, ⟨i.1, lt_of_lt_of_le i.2 h⟩, λ a b h,
  have _, from fin.veq_of_eq h, fin.eq_of_veq this⟩⟩⟩

@[simp] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=
by simp [lt_iff_le_not_le, -not_le]

@[simp] theorem nat_cast_inj {m n : ℕ} : (m : cardinal) = n ↔ m = n :=
by simp [le_antisymm_iff]

@[simp] theorem nat_succ (n : ℕ) : succ n = n.succ :=
le_antisymm (succ_le.2 $ nat_cast_lt.2 $ nat.lt_succ_self _) (add_one_le_succ _)

@[simp] theorem succ_zero : succ 0 = 1 :=
by simpa using nat_succ 0

theorem cantor' (a) {b : cardinal} (hb : 1 < b) : a < b ^ a :=
by rw [← succ_le, (by simpa using nat_succ 1 : succ 1 = 2)] at hb;
   exact lt_of_lt_of_le (cantor _) (power_le_power_right hb)

theorem one_le_iff_pos {c : cardinal} : 1 ≤ c ↔ 0 < c :=
by rw [← succ_zero, succ_le]

theorem one_le_iff_ne_zero {c : cardinal} : 1 ≤ c ↔ c ≠ 0 :=
by rw [one_le_iff_pos, pos_iff_ne_zero]

theorem nat_lt_omega (n : ℕ) : (n : cardinal.{u}) < omega :=
succ_le.1 $ by rw [nat_succ, ← lift_mk_fin, omega, lift_mk_le.{0 0 u}]; exact
⟨⟨fin.val, λ a b, fin.eq_of_veq⟩⟩

theorem one_lt_omega : 1 < omega :=
by simpa using nat_lt_omega 1

theorem lt_omega {c : cardinal.{u}} : c < omega ↔ ∃ n : ℕ, c = n :=
⟨λ h, begin
  rcases lt_lift_iff.1 h with ⟨c, rfl, h'⟩,
  rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩,
  suffices : finite S,
  { cases this, resetI,
    existsi fintype.card S,
    rw [← lift_nat_cast.{0 u}, lift_inj, fintype_card S] },
  by_contra nf,
  have P : ∀ (n : ℕ) (IH : ∀ i<n, S), ∃ a : S, ¬ ∃ y h, IH y h = a :=
    λ n IH,
    let g : {i | i < n} → S := λ ⟨i, h⟩, IH i h in
    classical.not_forall.1 (λ h, nf
      ⟨fintype.of_surjective g (λ a, subtype.exists.2 (h a))⟩),
  let F : ℕ → S := nat.lt_wf.fix (λ n IH, classical.some (P n IH)),
  refine not_le_of_lt h' ⟨⟨F, _⟩⟩,
  suffices : ∀ (n : ℕ) (m < n), F m ≠ F n,
  { refine λ m n, not_imp_not.1 (λ ne, _),
    rcases lt_trichotomy m n with h|h|h,
    { exact this n m h },
    { contradiction },
    { exact (this m n h).symm } },
  intros n m h,
  have := classical.some_spec (P n (λ y _, F y)),
  rw [← show F n = classical.some (P n (λ y _, F y)),
      from nat.lt_wf.fix_eq (λ n IH, classical.some (P n IH)) n] at this,
  exact λ e, this ⟨m, h, e⟩,
end, λ ⟨n, e⟩, e.symm ▸ nat_lt_omega _⟩

theorem omega_le {c : cardinal.{u}} : omega ≤ c ↔ ∀ n : ℕ, (n:cardinal) ≤ c :=
⟨λ h n, le_trans (le_of_lt (nat_lt_omega _)) h,
 λ h, le_of_not_lt $ λ hn, begin
  rcases lt_omega.1 hn with ⟨n, rfl⟩,
  exact not_le_of_lt (nat.lt_succ_self _) (nat_cast_le.1 (h (n+1)))
end⟩

theorem lt_omega_iff_fintype {α : Type u} : mk α < omega ↔ nonempty (fintype α) :=
lt_omega.trans ⟨λ ⟨n, e⟩, begin
  rw [← lift_mk_fin n] at e,
  cases quotient.exact e with f,
  exact ⟨fintype.of_equiv _ f.symm⟩
end, λ ⟨_⟩, by exactI ⟨_, fintype_card _⟩⟩

theorem lt_omega_iff_finite {α} {S : set α} : mk S < omega ↔ finite S :=
lt_omega_iff_fintype

theorem add_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a + b < omega :=
match a, b, lt_omega.1 ha, lt_omega.1 hb with
| _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat.cast_add]; apply nat_lt_omega
end

theorem mul_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a * b < omega :=
match a, b, lt_omega.1 ha, lt_omega.1 hb with
| _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat.cast_mul]; apply nat_lt_omega
end

theorem power_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a ^ b < omega :=
match a, b, lt_omega.1 ha, lt_omega.1 hb with
| _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ := by rw [← nat_cast_pow]; apply nat_lt_omega
end

/-- König's theorem -/
theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
lt_of_not_ge $ λ ⟨F⟩, begin
  have : inhabited (Π (i : ι), (g i).out),
  { refine ⟨λ i, classical.choice $ ne_zero_iff_nonempty.1 _⟩,
    rw mk_out,
    exact ne_of_gt (lt_of_le_of_lt (zero_le _) (H i)) }, resetI,
  let G := inv_fun F,
  have sG : surjective G := inv_fun_surjective F.2,
  choose C hc using show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b,
  { assume i,
    simp only [- not_exists, not_exists.symm, classical.not_forall.symm],
    refine λ h, not_le_of_lt (H i) _,
    rw [← mk_out (f i), ← mk_out (g i)],
    exact ⟨embedding.of_surjective h⟩ },
  exact (let ⟨⟨i, a⟩, h⟩ := sG C in hc i a (congr_fun h _))
end

@[simp] theorem mk_empty : mk empty = 0 :=
fintype_card empty

@[simp] theorem mk_pempty : mk pempty = 0 :=
fintype_card pempty

@[simp] theorem mk_plift_of_false {p : Prop} (h : ¬ p) : mk (plift p) = 0 :=
quotient.sound ⟨equiv.plift.trans $ equiv.equiv_pempty h⟩

@[simp] theorem mk_unit : mk unit = 1 :=
(fintype_card unit).trans nat.cast_one

@[simp] theorem mk_punit : mk punit = 1 :=
(fintype_card punit).trans nat.cast_one

@[simp] theorem mk_singleton {α : Type u} (x : α) : mk ({x} : set α) = 1 :=
quotient.sound ⟨equiv.set.singleton x⟩

@[simp] theorem mk_plift_of_true {p : Prop} (h : p) : mk (plift p) = 1 :=
quotient.sound ⟨equiv.plift.trans $ equiv.prop_equiv_punit h⟩

@[simp] theorem mk_bool : mk bool = 2 :=
quotient.sound ⟨equiv.bool_equiv_punit_sum_punit⟩

@[simp] theorem mk_Prop : mk Prop = 2 :=
(quotient.sound ⟨equiv.Prop_equiv_bool⟩ : mk Prop = mk bool).trans mk_bool

@[simp] theorem mk_option {α : Type u} : mk (option α) = mk α + 1 :=
quotient.sound ⟨equiv.option_equiv_sum_punit α⟩

theorem mk_list_eq_sum_pow (α : Type u) : mk (list α) = sum (λ n : ℕ, (mk α)^(n:cardinal.{u})) :=
calc  mk (list α)
    = mk (Σ n, vector α n) : quotient.sound ⟨equiv.equiv_sigma_subtype list.length⟩
... = mk (Σ n, fin n → α) : quotient.sound ⟨equiv.sigma_congr_right $ λ n,
  ⟨vector.nth, vector.of_fn, vector.of_fn_nth, λ f, funext $ vector.nth_of_fn f⟩⟩
... = mk (Σ n : ℕ, ulift.{u} (fin n) → α) : quotient.sound ⟨equiv.sigma_congr_right $ λ n,
  equiv.arrow_congr equiv.ulift.symm (equiv.refl α)⟩
... = sum (λ n : ℕ, (mk α)^(n:cardinal.{u})) : by simp only [(lift_mk_fin _).symm, lift_mk, power_def, sum_mk]

theorem mk_quot_le {α : Type u} {r : α → α → Prop} : mk (quot r) ≤ mk α :=
mk_le_of_surjective quot.exists_rep

theorem mk_quotient_le {α : Type u} {s : setoid α} : mk (quotient s) ≤ mk α :=
mk_quot_le

theorem mk_subtype_le {α : Type u} {s : set α} : mk s ≤ mk α :=
mk_le_of_injective subtype.val_injective

@[simp] theorem mk_emptyc (α : Type u) : mk (∅ : set α) = 0 :=
quotient.sound ⟨equiv.set.pempty α⟩

theorem mk_univ {α : Type u} : mk (@univ α) = mk α :=
quotient.sound ⟨equiv.set.univ α⟩

theorem mk_image_le {α β : Type u} {f : α → β} {s : set α} : mk (f '' s) ≤ mk s :=
mk_le_of_surjective surjective_onto_image

theorem mk_range_le {α β : Type u} {f : α → β} {s : set α} : mk (range f) ≤ mk α :=
mk_le_of_surjective surjective_onto_range

theorem mk_eq_of_injective {α β : Type u} {f : α → β} {s : set α} (hf : injective f) :
  mk (f '' s) = mk s :=
quotient.sound ⟨(equiv.set.image f s hf).symm⟩

theorem mk_Union_le_sum_mk {α ι : Type u} {f : ι → set α} : mk (⋃ i, f i) ≤ sum (λ i, mk (f i)) :=
calc mk (⋃ i, f i) ≤ mk (Σ i, f i) : mk_le_of_surjective (set.surjective_sigma_to_Union f)
  ... = sum (λ i, mk (f i)) : (sum_mk _).symm

theorem mk_Union_eq_sum_mk {α ι : Type u} {f : ι → set α} (h : ∀i j, i ≠ j → disjoint (f i) (f j)) :
  mk (⋃ i, f i) = sum (λ i, mk (f i)) :=
calc mk (⋃ i, f i) = mk (Σi, f i) : quot.sound ⟨set.Union_eq_sigma_of_disjoint h⟩
  ... = sum (λi, mk (f i)) : (sum_mk _).symm

@[simp] lemma finset_card {α : Type u} {s : finset α} : ↑(finset.card s) = mk (↑s : set α) :=
by rw [fintype_card, nat_cast_inj, fintype.card_coe]

theorem mk_union_add_mk_inter {α : Type u} {S T : set α} : mk (S ∪ T : set α) + mk (S ∩ T : set α) = mk S + mk T :=
quot.sound ⟨equiv.set.union_sum_inter S T⟩

theorem mk_union_of_disjoint {α : Type u} {S T : set α} (H : disjoint S T) : mk (S ∪ T : set α) = mk S + mk T :=
quot.sound ⟨equiv.set.union (disjoint_iff.1 H)⟩

lemma mk_le_mk_of_subset {α} {s t : set α} (h : s ⊆ t) : mk s ≤ mk t :=
⟨ set.embedding_of_subset h ⟩

end cardinal


text:
import .mat data.real.basic

-- To do : update using mat

#exit

open matrix

variables {k m n : nat}

namespace sdp

def S (n : nat) : Type := matrix real n n

structure primal (m n : nat) :=
(obf : S n)
(lhs : vector (S n) m)
(rhs : vector real m)

def primal.feasible (P : primal m n) (X : S n) : Prop :=
let ⟨C,A,b⟩ := P in
(∀ i : fin m, ⟪A.nth i, X⟫ = b.nth i) ∧ (0 ≼ X)

def primal.optimal (P : primal m n) (X : S n) : Prop :=
let C := P.obf in
primal.feasible P X ∧ (∀ Y : S n, primal.feasible P Y → ⟪C, X⟫ ≤ ⟪C, Y⟫)

structure dual (m n : nat) :=
(obf : vector real m)
(lhs : vector (S n) m)
(rhs : S n)

def dual.feasible (D : dual m n) (y : vector real m) : Prop :=
let ⟨b,A,C⟩ := D in
(vector.map₂ const_mul y A).sum ≼ C

def dual.optimal (D : dual m n) (y : vector real m) : Prop :=
let b := D.obf in
dual.feasible D y ∧ (∀ x : vector real m, dual.feasible D x → (b ⬝ x) ≤ (b ⬝ y))

def primal.to_dual : primal m n → dual m n
| ⟨C,A,b⟩ := ⟨b,A,C⟩

/- Lemma 2.12 -/
lemma optimality_condition (C A b) (X : S n) (y : vector real m) :
  primal.feasible ⟨C,A,b⟩ X → dual.feasible ⟨b,A,C⟩ y →
  mul (C - (vector.map₂ const_mul y A).sum) X = 0 →
  (primal.optimal ⟨C,A,b⟩ X ∧ dual.optimal ⟨b,A,C⟩ y) := sorry

def primal.strictly_feasible (P : primal m n) (X : S n) : Prop :=
let ⟨C,A,b⟩ := P in
(∀ i : fin m, ⟪A.nth i, X⟫ = b.nth i) ∧ (0 ≺ X)

def dual.strictly_feasible (D : dual m n) (y : vector real m) : Prop :=
let ⟨b,A,C⟩ := D in
(vector.map₂ const_mul y A).sum ≺ C

/- Lemma 2.15 -/
lemma no_duality_gap (C : S n) (A : vector (S n) m) (b : vector real m) :
  (∃ X : S n, primal.strictly_feasible ⟨C,A,b⟩ X) →
  (∃ y : vector real m, dual.strictly_feasible ⟨b,A,C⟩ y) →
  (∃ X : S n, ∃ y : vector real m,
    ( primal.optimal ⟨C,A,b⟩ X ∧
      dual.optimal ⟨b,A,C⟩ y ∧ ⟪C, X⟫ = b ⬝ y ) ) := sorry

end sdp

author: skbaek

repo: cvx

save_path: github-repos/lean/skbaek-cvx


text:
/-
Copyright (c) 2022 Jireh Loreaux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jireh Loreaux

! This file was ported from Lean 3 source module topology.continuous_function.units
! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Analysis.NormedSpace.Units
import Mathbin.Algebra.Algebra.Spectrum
import Mathbin.Topology.ContinuousFunction.Algebra

/-!
# Units of continuous functions

This file concerns itself with `C(X, M)ˣ` and `C(X, Mˣ)` when `X` is a topological space
and `M` has some monoid structure compatible with its topology.
-/

variable {X M R 𝕜 : Type _} [TopologicalSpace X]

namespace ContinuousMap

section Monoid

variable [Monoid M] [TopologicalSpace M] [ContinuousMul M]

/-- Equivalence between continuous maps into the units of a monoid with continuous multiplication
and the units of the monoid of continuous maps. -/
@[to_additive
      "Equivalence between continuous maps into the additive units of an additive monoid\nwith continuous addition and the additive units of the additive monoid of continuous maps.",
  simps]
def unitsLift : C(X, Mˣ) ≃ C(X, M)ˣ
    where
  toFun f :=
    { val := ⟨fun x => f x, Units.continuous_val.comp f.Continuous⟩
      inv := ⟨fun x => ↑(f x)⁻¹, Units.continuous_val.comp (continuous_inv.comp f.Continuous)⟩
      val_inv := ext fun x => Units.mul_inv _
      inv_val := ext fun x => Units.inv_mul _ }
  invFun f :=
    { toFun := fun x =>
        ⟨f x, f⁻¹ x, ContinuousMap.congr_fun f.mul_inv x, ContinuousMap.congr_fun f.inv_mul x⟩
      continuous_toFun :=
        continuous_induced_rng.2 <|
          Continuous.prod_mk (f : C(X, M)).Continuous <|
            MulOpposite.continuous_op.comp (↑f⁻¹ : C(X, M)).Continuous }
  left_inv f := by
    ext
    rfl
  right_inv f := by
    ext
    rfl
#align continuous_map.units_lift ContinuousMap.unitsLift
#align continuous_map.add_units_lift ContinuousMap.addUnitsLift

end Monoid

section NormedRing

variable [NormedRing R] [CompleteSpace R]

theorem NormedRing.isUnit_unit_continuous {f : C(X, R)} (h : ∀ x, IsUnit (f x)) :
    Continuous fun x => (h x).Unit :=
  by
  refine'
    continuous_induced_rng.2
      (Continuous.prod_mk f.continuous
        (mul_opposite.continuous_op.comp (continuous_iff_continuous_at.mpr fun x => _)))
  have := NormedRing.inverse_continuousAt (h x).Unit
  simp only [← Ring.inverse_unit, IsUnit.unit_spec, ← Function.comp_apply] at this⊢
  exact this.comp (f.continuous_at x)
#align normed_ring.is_unit_unit_continuous NormedRing.isUnit_unit_continuous

/-- Construct a continuous map into the group of units of a normed ring from a function into the
normed ring and a proof that every element of the range is a unit. -/
@[simps]
noncomputable def unitsOfForallIsUnit {f : C(X, R)} (h : ∀ x, IsUnit (f x)) : C(X, Rˣ)
    where
  toFun x := (h x).Unit
  continuous_toFun := NormedRing.isUnit_unit_continuous h
#align continuous_map.units_of_forall_is_unit ContinuousMap.unitsOfForallIsUnit

instance canLift :
    CanLift C(X, R) C(X, Rˣ) (fun f => ⟨fun x => f x, Units.continuous_val.comp f.Continuous⟩)
      fun f => ∀ x, IsUnit (f x)
    where prf f h :=
    ⟨unitsOfForallIsUnit h, by
      ext
      rfl⟩
#align continuous_map.can_lift ContinuousMap.canLift

theorem isUnit_iff_forall_isUnit (f : C(X, R)) : IsUnit f ↔ ∀ x, IsUnit (f x) :=
  Iff.intro (fun h => fun x => ⟨unitsLift.symm h.Unit x, rfl⟩) fun h =>
    ⟨(unitsOfForallIsUnit h).unitsLift, by
      ext
      rfl⟩
#align continuous_map.is_unit_iff_forall_is_unit ContinuousMap.isUnit_iff_forall_isUnit

end NormedRing

section NormedField

variable [NormedField 𝕜] [CompleteSpace 𝕜]

theorem isUnit_iff_forall_ne_zero (f : C(X, 𝕜)) : IsUnit f ↔ ∀ x, f x ≠ 0 := by
  simp_rw [f.is_unit_iff_forall_is_unit, isUnit_iff_ne_zero]
#align continuous_map.is_unit_iff_forall_ne_zero ContinuousMap.isUnit_iff_forall_ne_zero

theorem spectrum_eq_range (f : C(X, 𝕜)) : spectrum 𝕜 f = Set.range f :=
  by
  ext
  simp only [spectrum.mem_iff, is_unit_iff_forall_ne_zero, not_forall, coe_sub, Pi.sub_apply,
    algebraMap_apply, Algebra.id.smul_eq_mul, mul_one, Classical.not_not, Set.mem_range,
    sub_eq_zero, @eq_comm _ x _]
#align continuous_map.spectrum_eq_range ContinuousMap.spectrum_eq_range

end NormedField

end ContinuousMap

author: leanprover-community


text:
import game.world3.level2 -- hide
import mynat.mul -- hide

namespace mynat -- hide

/-
# Multiplication World

## Level 3: `one_mul`

These proofs from addition world might be useful here:

* `one_eq_succ_zero : 1 = succ(0)`
* `succ_eq_add_one a : succ(a) = a + 1`

We just proved `mul_one`, now let's prove `one_mul`.
Then we will have proved, in fancy terms,
that 1 is a "left and right identity"
for multiplication (just like we showed that
0 is a left and right identity for addition
with `add_zero` and `zero_add`).
-/

/- Lemma
For any natural number $m$, we have
$$ 1 \times m = m. $$
-/
lemma one_mul (m : mynat) : 1 * m = m :=
begin [nat_num_game]
  induction m with d hd,
  {
    rw mul_zero,
    refl,
  },
  {
    rw mul_succ,
    rw hd,
    rw succ_eq_add_one,
    refl,
  }
end

end mynat -- hide

author: ImperialCollegeLondon


text:
/-
Copyright (c) 2021 Benjamin Davidson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Benjamin Davidson
-/
import measure_theory.integral.interval_integral
import analysis.special_functions.trigonometric.arctan_deriv

/-!
# Integration of specific interval integrals

This file contains proofs of the integrals of various specific functions. This includes:
* Integrals of simple functions, such as `id`, `pow`, `inv`, `exp`, `log`
* Integrals of some trigonometric functions, such as `sin`, `cos`, `1 / (1 + x^2)`
* The integral of `cos x ^ 2 - sin x ^ 2`
* Reduction formulae for the integrals of `sin x ^ n` and `cos x ^ n` for `n ≥ 2`
* The computation of `∫ x in 0..π, sin x ^ n` as a product for even and odd `n` (used in proving the
  Wallis product for pi)
* Integrals of the form `sin x ^ m * cos x ^ n`

With these lemmas, many simple integrals can be computed by `simp` or `norm_num`.
See `test/integration.lean` for specific examples.

This file also contains some facts about the interval integrability of specific functions.

This file is still being developed.

## Tags

integrate, integration, integrable, integrability
-/

open real nat set finset
open_locale real big_operators interval
variables {a b : ℝ} (n : ℕ)

namespace interval_integral
open measure_theory
variables {f : ℝ → ℝ} {μ ν : measure ℝ} [is_locally_finite_measure μ] (c d : ℝ)

/-! ### Interval integrability -/

@[simp]
lemma interval_integrable_pow : interval_integrable (λ x, x^n) μ a b :=
(continuous_pow n).interval_integrable a b

lemma interval_integrable_zpow {n : ℤ} (h : 0 ≤ n ∨ (0 : ℝ) ∉ [a, b]) :
  interval_integrable (λ x, x ^ n) μ a b :=
(continuous_on_id.zpow n $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable

lemma interval_integrable_rpow {r : ℝ} (h : 0 ≤ r ∨ (0 : ℝ) ∉ [a, b]) :
  interval_integrable (λ x, x ^ r) μ a b :=
(continuous_on_id.rpow_const $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable

@[simp]
lemma interval_integrable_id : interval_integrable (λ x, x) μ a b :=
continuous_id.interval_integrable a b

@[simp]
lemma interval_integrable_const : interval_integrable (λ x, c) μ a b :=
continuous_const.interval_integrable a b

@[simp]
lemma interval_integrable.const_mul (h : interval_integrable f ν a b) :
  interval_integrable (λ x, c * f x) ν a b :=
by convert h.smul c

@[simp]
lemma interval_integrable.mul_const (h : interval_integrable f ν a b) :
  interval_integrable (λ x, f x * c) ν a b :=
by simp only [mul_comm, interval_integrable.const_mul c h]

@[simp]
lemma interval_integrable.div (h : interval_integrable f ν a b) :
  interval_integrable (λ x, f x / c) ν a b :=
interval_integrable.mul_const c⁻¹ h

lemma interval_integrable_one_div (h : ∀ x : ℝ, x ∈ [a, b] → f x ≠ 0)
  (hf : continuous_on f [a, b]) :
  interval_integrable (λ x, 1 / f x) μ a b :=
(continuous_on_const.div hf h).interval_integrable

@[simp]
lemma interval_integrable_inv (h : ∀ x : ℝ, x ∈ [a, b] → f x ≠ 0)
  (hf : continuous_on f [a, b]) :
  interval_integrable (λ x, (f x)⁻¹) μ a b :=
by simpa only [one_div] using interval_integrable_one_div h hf

@[simp]
lemma interval_integrable_exp : interval_integrable exp μ a b :=
continuous_exp.interval_integrable a b

@[simp]
lemma interval_integrable.log
  (hf : continuous_on f [a, b]) (h : ∀ x : ℝ, x ∈ [a, b] → f x ≠ 0) :
  interval_integrable (λ x, log (f x)) μ a b :=
(continuous_on.log hf h).interval_integrable

@[simp]
lemma interval_integrable_log (h : (0:ℝ) ∉ [a, b]) :
  interval_integrable log μ a b :=
interval_integrable.log continuous_on_id $ λ x hx, ne_of_mem_of_not_mem hx h

@[simp]
lemma interval_integrable_sin : interval_integrable sin μ a b :=
continuous_sin.interval_integrable a b

@[simp]
lemma interval_integrable_cos : interval_integrable cos μ a b :=
continuous_cos.interval_integrable a b

lemma interval_integrable_one_div_one_add_sq : interval_integrable (λ x : ℝ, 1 / (1 + x^2)) μ a b :=
begin
  refine (continuous_const.div _ (λ x, _)).interval_integrable a b,
  { continuity },
  { nlinarith },
end

@[simp]
lemma interval_integrable_inv_one_add_sq : interval_integrable (λ x : ℝ, (1 + x^2)⁻¹) μ a b :=
by simpa only [one_div] using interval_integrable_one_div_one_add_sq

/-! ### Integrals of the form `c * ∫ x in a..b, f (c * x + d)` -/

@[simp]
lemma mul_integral_comp_mul_right : c * ∫ x in a..b, f (x * c) = ∫ x in a*c..b*c, f x :=
smul_integral_comp_mul_right f c

@[simp]
lemma mul_integral_comp_mul_left : c * ∫ x in a..b, f (c * x) = ∫ x in c*a..c*b, f x :=
smul_integral_comp_mul_left f c

@[simp]
lemma inv_mul_integral_comp_div : c⁻¹ * ∫ x in a..b, f (x / c) = ∫ x in a/c..b/c, f x :=
inv_smul_integral_comp_div f c

@[simp]
lemma mul_integral_comp_mul_add : c * ∫ x in a..b, f (c * x + d) = ∫ x in c*a+d..c*b+d, f x :=
smul_integral_comp_mul_add f c d

@[simp]
lemma mul_integral_comp_add_mul : c * ∫ x in a..b, f (d + c * x) = ∫ x in d+c*a..d+c*b, f x :=
smul_integral_comp_add_mul f c d

@[simp]
lemma inv_mul_integral_comp_div_add : c⁻¹ * ∫ x in a..b, f (x / c + d) = ∫ x in a/c+d..b/c+d, f x :=
inv_smul_integral_comp_div_add f c d

@[simp]
lemma inv_mul_integral_comp_add_div : c⁻¹ * ∫ x in a..b, f (d + x / c) = ∫ x in d+a/c..d+b/c, f x :=
inv_smul_integral_comp_add_div f c d

@[simp]
lemma mul_integral_comp_mul_sub : c * ∫ x in a..b, f (c * x - d) = ∫ x in c*a-d..c*b-d, f x :=
smul_integral_comp_mul_sub f c d

@[simp]
lemma mul_integral_comp_sub_mul : c * ∫ x in a..b, f (d - c * x) = ∫ x in d-c*b..d-c*a, f x :=
smul_integral_comp_sub_mul f c d

@[simp]
lemma inv_mul_integral_comp_div_sub : c⁻¹ * ∫ x in a..b, f (x / c - d) = ∫ x in a/c-d..b/c-d, f x :=
inv_smul_integral_comp_div_sub f c d

@[simp]
lemma inv_mul_integral_comp_sub_div : c⁻¹ * ∫ x in a..b, f (d - x / c) = ∫ x in d-b/c..d-a/c, f x :=
inv_smul_integral_comp_sub_div f c d

end interval_integral

open interval_integral

/-! ### Integrals of simple functions -/

lemma integral_rpow {r : ℝ} (h : 0 ≤ r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [a, b]) :
  ∫ x in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) :=
begin
  suffices : ∀ x ∈ [a, b], has_deriv_at (λ x : ℝ, x ^ (r + 1) / (r + 1)) (x ^ r) x,
  { rw sub_div,
    exact integral_eq_sub_of_has_deriv_at this (interval_integrable_rpow (h.imp_right and.right)) },
  intros x hx,
  have hx' : x ≠ 0 ∨ 1 ≤ r + 1,
    from h.symm.imp (λ h, ne_of_mem_of_not_mem hx h.2) (le_add_iff_nonneg_left _).2,
  convert (real.has_deriv_at_rpow_const hx').div_const (r + 1),
  rw [add_sub_cancel, mul_div_cancel_left],
  rw [ne.def, ← eq_neg_iff_add_eq_zero],
  rintro rfl,
  apply (@zero_lt_one ℝ _ _).not_le,
  simpa using h
end

lemma integral_zpow {n : ℤ} (h : 0 ≤ n ∨ n ≠ -1 ∧ (0 : ℝ) ∉ [a, b]) :
  ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
begin
  replace h : 0 ≤ (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [a, b], by exact_mod_cast h,
  exact_mod_cast integral_rpow h
end

@[simp] lemma integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
by simpa using integral_zpow (or.inl (int.coe_nat_nonneg n))

/-- Integral of `|x - a| ^ n` over `Ι a b`. This integral appears in the proof of the
Picard-Lindelöf/Cauchy-Lipschitz theorem. -/
lemma integral_pow_abs_sub_interval_oc :
  ∫ x in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (n + 1) :=
begin
  cases le_or_lt a b with hab hab,
  { calc ∫ x in Ι a b, |x - a| ^ n = ∫ x in a..b, |x - a| ^ n :
      by rw [interval_oc_of_le hab, ← integral_of_le hab]
    ... = ∫ x in 0..(b - a), x ^ n :
      begin
        simp only [integral_comp_sub_right (λ x, |x| ^ n), sub_self],
        refine integral_congr (λ x hx, congr_arg2 has_pow.pow (abs_of_nonneg $ _) rfl),
        rw interval_of_le (sub_nonneg.2 hab) at hx,
        exact hx.1
      end
    ... = |b - a| ^ (n + 1) / (n + 1) : by simp [abs_of_nonneg (sub_nonneg.2 hab)] },
  { calc ∫ x in Ι a b, |x - a| ^ n = ∫ x in b..a, |x - a| ^ n :
      by rw [interval_oc_of_lt hab, ← integral_of_le hab.le]
    ... = ∫ x in b - a..0, (-x) ^ n :
      begin
        simp only [integral_comp_sub_right (λ x, |x| ^ n), sub_self],
        refine integral_congr (λ x hx, congr_arg2 has_pow.pow (abs_of_nonpos $ _) rfl),
        rw interval_of_le (sub_nonpos.2 hab.le) at hx,
        exact hx.2
      end
    ... = |b - a| ^ (n + 1) / (n + 1) :
      by simp [integral_comp_neg (λ x, x ^ n), abs_of_neg (sub_neg.2 hab)] }
end

@[simp]
lemma integral_id : ∫ x in a..b, x = (b ^ 2 - a ^ 2) / 2 :=
by simpa using integral_pow 1

@[simp]
lemma integral_one : ∫ x in a..b, (1 : ℝ) = b - a :=
by simp only [mul_one, smul_eq_mul, integral_const]

@[simp]
lemma integral_inv (h : (0:ℝ) ∉ [a, b]) : ∫ x in a..b, x⁻¹ = log (b / a) :=
begin
  have h' := λ x hx, ne_of_mem_of_not_mem hx h,
  rw [integral_deriv_eq_sub' _ deriv_log' (λ x hx, differentiable_at_log (h' x hx))
        (continuous_on_inv₀.mono $ subset_compl_singleton_iff.mpr h),
      log_div (h' b right_mem_interval) (h' a left_mem_interval)],
end

@[simp]
lemma integral_inv_of_pos (ha : 0 < a) (hb : 0 < b) : ∫ x in a..b, x⁻¹ = log (b / a) :=
integral_inv $ not_mem_interval_of_lt ha hb

@[simp]
lemma integral_inv_of_neg (ha : a < 0) (hb : b < 0) : ∫ x in a..b, x⁻¹ = log (b / a) :=
integral_inv $ not_mem_interval_of_gt ha hb

lemma integral_one_div (h : (0:ℝ) ∉ [a, b]) : ∫ x : ℝ in a..b, 1/x = log (b / a) :=
by simp only [one_div, integral_inv h]

lemma integral_one_div_of_pos (ha : 0 < a) (hb : 0 < b) : ∫ x : ℝ in a..b, 1/x = log (b / a) :=
by simp only [one_div, integral_inv_of_pos ha hb]

lemma integral_one_div_of_neg (ha : a < 0) (hb : b < 0) : ∫ x : ℝ in a..b, 1/x = log (b / a) :=
by simp only [one_div, integral_inv_of_neg ha hb]

@[simp]
lemma integral_exp : ∫ x in a..b, exp x = exp b - exp a :=
by rw integral_deriv_eq_sub'; norm_num [continuous_on_exp]

@[simp]
lemma integral_log (h : (0:ℝ) ∉ [a, b]) :
  ∫ x in a..b, log x = b * log b - a * log a - b + a :=
begin
  obtain ⟨h', heq⟩ := ⟨λ x hx, ne_of_mem_of_not_mem hx h, λ x hx, mul_inv_cancel (h' x hx)⟩,
  convert integral_mul_deriv_eq_deriv_mul (λ x hx, has_deriv_at_log (h' x hx))
      (λ x hx, has_deriv_at_id x)
      (continuous_on_inv₀.mono $ subset_compl_singleton_iff.mpr h).interval_integrable
      continuous_on_const.interval_integrable using 1;
    simp [integral_congr heq, mul_comm, ← sub_add],
end

@[simp]
lemma integral_log_of_pos (ha : 0 < a) (hb : 0 < b) :
  ∫ x in a..b, log x = b * log b - a * log a - b + a :=
integral_log $ not_mem_interval_of_lt ha hb

@[simp]
lemma integral_log_of_neg (ha : a < 0) (hb : b < 0) :
  ∫ x in a..b, log x = b * log b - a * log a - b + a :=
integral_log $ not_mem_interval_of_gt ha hb

@[simp]
lemma integral_sin : ∫ x in a..b, sin x = cos a - cos b :=
by rw integral_deriv_eq_sub' (λ x, -cos x); norm_num [continuous_on_sin]

@[simp]
lemma integral_cos : ∫ x in a..b, cos x = sin b - sin a :=
by rw integral_deriv_eq_sub'; norm_num [continuous_on_cos]

lemma integral_cos_sq_sub_sin_sq :
  ∫ x in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a :=
by simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using integral_deriv_mul_eq_sub
  (λ x hx, has_deriv_at_sin x) (λ x hx, has_deriv_at_cos x) continuous_on_cos.interval_integrable
  continuous_on_sin.neg.interval_integrable

@[simp]
lemma integral_inv_one_add_sq : ∫ x : ℝ in a..b, (1 + x^2)⁻¹ = arctan b - arctan a :=
begin
  simp only [← one_div],
  refine integral_deriv_eq_sub' _ _ _ (continuous_const.div _ (λ x, _)).continuous_on,
  { norm_num },
  { norm_num },
  { continuity },
  { nlinarith },
end

lemma integral_one_div_one_add_sq : ∫ x : ℝ in a..b, 1 / (1 + x^2) = arctan b - arctan a :=
by simp only [one_div, integral_inv_one_add_sq]

/-! ### Integral of `sin x ^ n` -/

lemma integral_sin_pow_aux :
  ∫ x in a..b, sin x ^ (n + 2) = sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
    + (n + 1) * (∫ x in a..b, sin x ^ n) - (n + 1) * ∫ x in a..b, sin x ^ (n + 2) :=
begin
  let C := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b,
  have h : ∀ α β γ : ℝ, α * (β * α * γ) = β * (α * α * γ) := λ α β γ, by ring,
  have hu : ∀ x ∈ _, has_deriv_at (λ y, sin y ^ (n + 1)) ((n + 1) * cos x * sin x ^ n) x :=
    λ x hx, by simpa only [mul_right_comm] using (has_deriv_at_sin x).pow,
  have hv : ∀ x ∈ [a, b], has_deriv_at (-cos) (sin x) x :=
    λ x hx, by simpa only [neg_neg] using (has_deriv_at_cos x).neg,
  have H := integral_mul_deriv_eq_deriv_mul hu hv _ _,
  calc  ∫ x in a..b, sin x ^ (n + 2)
      = ∫ x in a..b, sin x ^ (n + 1) * sin x                   : by simp only [pow_succ']
  ... = C + (n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n       : by simp [H, h, sq]
  ... = C + (n + 1) * ∫ x in a..b, sin x ^ n - sin x ^ (n + 2) : by simp [cos_sq', sub_mul,
                                                                          ← pow_add, add_comm]
  ... = C + (n + 1) * (∫ x in a..b, sin x ^ n) - (n + 1) * ∫ x in a..b, sin x ^ (n + 2) :
    by rw [integral_sub, mul_sub, add_sub_assoc]; apply continuous.interval_integrable; continuity,
  all_goals { apply continuous.interval_integrable, continuity },
end

/-- The reduction formula for the integral of `sin x ^ n` for any natural `n ≥ 2`. -/
lemma integral_sin_pow :
  ∫ x in a..b, sin x ^ (n + 2) = (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (n + 2)
    + (n + 1) / (n + 2) * ∫ x in a..b, sin x ^ n :=
begin
  have : (n : ℝ) + 2 ≠ 0 := by exact_mod_cast succ_ne_zero n.succ,
  field_simp,
  convert eq_sub_iff_add_eq.mp (integral_sin_pow_aux n),
  ring,
end

@[simp]
lemma integral_sin_sq : ∫ x in a..b, sin x ^ 2 = (sin a * cos a - sin b * cos b + b - a) / 2 :=
by field_simp [integral_sin_pow, add_sub_assoc]

theorem integral_sin_pow_odd :
  ∫ x in 0..π, sin x ^ (2 * n + 1) = 2 * ∏ i in range n, (2 * i + 2) / (2 * i + 3) :=
begin
  induction n with k ih, { norm_num },
  rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow],
  norm_cast,
  simp [-cast_add] with field_simps,
end

theorem integral_sin_pow_even :
  ∫ x in 0..π, sin x ^ (2 * n) = π * ∏ i in range n, (2 * i + 1) / (2 * i + 2) :=
begin
  induction n with k ih, { simp },
  rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow],
  norm_cast,
  simp [-cast_add] with field_simps,
end

lemma integral_sin_pow_pos : 0 < ∫ x in 0..π, sin x ^ n :=
begin
  rcases even_or_odd' n with ⟨k, (rfl | rfl)⟩;
  simp only [integral_sin_pow_even, integral_sin_pow_odd];
  refine mul_pos (by norm_num [pi_pos]) (prod_pos (λ n hn, div_pos _ _));
  norm_cast;
  linarith,
end

lemma integral_sin_pow_succ_le : ∫ x in 0..π, sin x ^ (n + 1) ≤ ∫ x in 0..π, sin x ^ n :=
let H := λ x h, pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1) in
by refine integral_mono_on pi_pos.le _ _ H; exact (continuous_sin.pow _).interval_integrable 0 π

lemma integral_sin_pow_antitone : antitone (λ n : ℕ, ∫ x in 0..π, sin x ^ n) :=
antitone_nat_of_succ_le integral_sin_pow_succ_le

/-! ### Integral of `cos x ^ n` -/

lemma integral_cos_pow_aux :
  ∫ x in a..b, cos x ^ (n + 2) = cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
    + (n + 1) * (∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) :=
begin
  let C := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a,
  have h : ∀ α β γ : ℝ, α * (β * α * γ) = β * (α * α * γ) := λ α β γ, by ring,
  have hu : ∀ x ∈ _, has_deriv_at (λ y, cos y ^ (n + 1)) (-(n + 1) * sin x * cos x ^ n) x :=
    λ x hx, by simpa only [mul_right_comm, neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm]
      using (has_deriv_at_cos x).pow,
  have hv : ∀ x ∈ [a, b], has_deriv_at sin (cos x) x := λ x hx, has_deriv_at_sin x,
  have H := integral_mul_deriv_eq_deriv_mul hu hv _ _,
  calc  ∫ x in a..b, cos x ^ (n + 2)
      = ∫ x in a..b, cos x ^ (n + 1) * cos x                   : by simp only [pow_succ']
  ... = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n       : by simp [H, h, sq, -neg_add_rev]
  ... = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) : by simp [sin_sq, sub_mul,
                                                                          ← pow_add, add_comm]
  ... = C + (n + 1) * (∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) :
    by rw [integral_sub, mul_sub, add_sub_assoc]; apply continuous.interval_integrable; continuity,
  all_goals { apply continuous.interval_integrable, continuity },
end

/-- The reduction formula for the integral of `cos x ^ n` for any natural `n ≥ 2`. -/
lemma integral_cos_pow :
  ∫ x in a..b, cos x ^ (n + 2) = (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (n + 2)
    + (n + 1) / (n + 2) * ∫ x in a..b, cos x ^ n :=
begin
  have : (n : ℝ) + 2 ≠ 0 := by exact_mod_cast succ_ne_zero n.succ,
  field_simp,
  convert eq_sub_iff_add_eq.mp (integral_cos_pow_aux n),
  ring,
end

@[simp]
lemma integral_cos_sq : ∫ x in a..b, cos x ^ 2 = (cos b * sin b - cos a * sin a + b - a) / 2 :=
by field_simp [integral_cos_pow, add_sub_assoc]

/-! ### Integral of `sin x ^ m * cos x ^ n` -/

/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `n` is odd. -/
lemma integral_sin_pow_mul_cos_pow_odd (m n : ℕ) :
  ∫ x in a..b, sin x ^ m * cos x ^ (2 * n + 1) = ∫ u in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n :=
have hc : continuous (λ u : ℝ, u ^ m * (1 - u ^ 2) ^ n), by continuity,
calc  ∫ x in a..b, sin x ^ m * cos x ^ (2 * n + 1)
    = ∫ x in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x : by simp only [pow_succ', ← mul_assoc,
                                                                           pow_mul, cos_sq']
... = ∫ u in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n         : integral_comp_mul_deriv
                                                              (λ x hx, has_deriv_at_sin x)
                                                                continuous_on_cos hc

/-- The integral of `sin x * cos x`, given in terms of sin².
  See `integral_sin_mul_cos₂` below for the integral given in terms of cos². -/
@[simp]
lemma integral_sin_mul_cos₁ :
  ∫ x in a..b, sin x * cos x = (sin b ^ 2 - sin a ^ 2) / 2 :=
by simpa using integral_sin_pow_mul_cos_pow_odd 1 0

@[simp]
lemma integral_sin_sq_mul_cos :
  ∫ x in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3 :=
by simpa using integral_sin_pow_mul_cos_pow_odd 2 0

@[simp]
lemma integral_cos_pow_three :
  ∫ x in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3 :=
by simpa using integral_sin_pow_mul_cos_pow_odd 0 1

/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` is odd. -/
lemma integral_sin_pow_odd_mul_cos_pow (m n : ℕ) :
  ∫ x in a..b, sin x ^ (2 * m + 1) * cos x ^ n = ∫ u in cos b..cos a, u ^ n * (1 - u ^ 2) ^ m :=
have hc : continuous (λ u : ℝ, u ^ n * (1 - u ^ 2) ^ m), by continuity,
calc   ∫ x in a..b, sin x ^ (2 * m + 1) * cos x ^ n
    = -∫ x in b..a, sin x ^ (2 * m + 1) * cos x ^ n          : by rw integral_symm
... =  ∫ x in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n : by simp [pow_succ', pow_mul, sin_sq]
... =  ∫ x in b..a, cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x : by { congr, ext, ring }
... =  ∫ u in cos b..cos a, u ^ n * (1 - u ^ 2) ^ m          : integral_comp_mul_deriv
                                                                (λ x hx, has_deriv_at_cos x)
                                                                  continuous_on_sin.neg hc

/-- The integral of `sin x * cos x`, given in terms of cos².
See `integral_sin_mul_cos₁` above for the integral given in terms of sin². -/
lemma integral_sin_mul_cos₂  :
  ∫ x in a..b, sin x * cos x = (cos a ^ 2 - cos b ^ 2) / 2 :=
by simpa using integral_sin_pow_odd_mul_cos_pow 0 1

@[simp]
lemma integral_sin_mul_cos_sq :
  ∫ x in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3 :=
by simpa using integral_sin_pow_odd_mul_cos_pow 0 2

@[simp]
lemma integral_sin_pow_three :
  ∫ x in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3 :=
by simpa using integral_sin_pow_odd_mul_cos_pow 1 0

/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` and `n` are both even. -/
lemma integral_sin_pow_even_mul_cos_pow_even (m n : ℕ) :
    ∫ x in a..b, sin x ^ (2 * m) * cos x ^ (2 * n)
  = ∫ x in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n :=
by field_simp [pow_mul, sin_sq, cos_sq, ← sub_sub, (by ring : (2:ℝ) - 1 = 1)]

@[simp]
lemma integral_sin_sq_mul_cos_sq :
  ∫ x in a..b, sin x ^ 2 * cos x ^ 2 = (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 :=
begin
  convert integral_sin_pow_even_mul_cos_pow_even 1 1 using 1,
  have h1 : ∀ c : ℝ, (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4 := λ c, by ring,
  have h2 : continuous (λ x, cos (2 * x) ^ 2) := by continuity,
  have h3 : ∀ x, cos x * sin x = sin (2 * x) / 2, { intro, rw sin_two_mul, ring },
  have h4 : ∀ d : ℝ, 2 * (2 * d) = 4 * d := λ d, by ring,
  simp [h1, h2.interval_integrable, integral_comp_mul_left (λ x, cos x ^ 2), h3, h4],
  ring,
end

author: Mel-TunaRoll

repo: Lean-Mordell-Weil-Mel-Branch


text:
/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Anne Baanen
-/
import algebra.group_with_zero.units.lemmas
import algebra.order.field.defs
import algebra.order.hom.basic
import algebra.order.ring.abs
import algebra.ring.commute
import algebra.ring.regular

/-!
# Absolute values

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

This file defines a bundled type of absolute values `absolute_value R S`.

## Main definitions

 * `absolute_value R S` is the type of absolute values on `R` mapping to `S`.
 * `absolute_value.abs` is the "standard" absolute value on `S`, mapping negative `x` to `-x`.
 * `absolute_value.to_monoid_with_zero_hom`: absolute values mapping to a
   linear ordered field preserve `0`, `*` and `1`
 * `is_absolute_value`: a type class stating that `f : β → α` satisfies the axioms of an abs val
-/

/-- `absolute_value R S` is the type of absolute values on `R` mapping to `S`:
the maps that preserve `*`, are nonnegative, positive definite and satisfy the triangle equality. -/
structure absolute_value (R S : Type*) [semiring R] [ordered_semiring S]
  extends R →ₙ* S :=
(nonneg' : ∀ x, 0 ≤ to_fun x)
(eq_zero' : ∀ x, to_fun x = 0 ↔ x = 0)
(add_le' : ∀ x y, to_fun (x + y) ≤ to_fun x + to_fun y)

namespace absolute_value

attribute [nolint doc_blame] absolute_value.to_mul_hom

section ordered_semiring

section semiring

variables {R S : Type*} [semiring R] [ordered_semiring S] (abv : absolute_value R S)

instance zero_hom_class : zero_hom_class (absolute_value R S) R S :=
{ coe := λ f, f.to_fun,
  coe_injective' := λ f g h, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' },
  map_zero := λ f, (f.eq_zero' _).2 rfl }

instance mul_hom_class : mul_hom_class (absolute_value R S) R S :=
{ map_mul := λ f, f.map_mul'
  ..absolute_value.zero_hom_class }

instance nonneg_hom_class : nonneg_hom_class (absolute_value R S) R S :=
{ map_nonneg := λ f, f.nonneg',
  ..absolute_value.zero_hom_class }

instance subadditive_hom_class : subadditive_hom_class (absolute_value R S) R S :=
{ map_add_le_add := λ f, f.add_le',
  ..absolute_value.zero_hom_class }

@[simp] lemma coe_mk (f : R →ₙ* S) {h₁ h₂ h₃} : ((absolute_value.mk f h₁ h₂ h₃) : R → S) = f := rfl

@[ext] lemma ext ⦃f g : absolute_value R S⦄ : (∀ x, f x = g x) → f = g := fun_like.ext _ _

/-- See Note [custom simps projection]. -/
def simps.apply (f : absolute_value R S) : R → S := f

initialize_simps_projections absolute_value (to_mul_hom_to_fun → apply)

/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
directly. -/
instance : has_coe_to_fun (absolute_value R S) (λ f, R → S) := fun_like.has_coe_to_fun

@[simp] lemma coe_to_mul_hom : ⇑abv.to_mul_hom = abv := rfl

protected theorem nonneg (x : R) : 0 ≤ abv x := abv.nonneg' x
@[simp] protected theorem eq_zero {x : R} : abv x = 0 ↔ x = 0 := abv.eq_zero' x
protected theorem add_le (x y : R) : abv (x + y) ≤ abv x + abv y := abv.add_le' x y
@[simp] protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y := abv.map_mul' x y

protected theorem ne_zero_iff {x : R} : abv x ≠ 0 ↔ x ≠ 0 := abv.eq_zero.not

protected theorem pos {x : R} (hx : x ≠ 0) : 0 < abv x :=
lt_of_le_of_ne (abv.nonneg x) (ne.symm $ mt abv.eq_zero.mp hx)

@[simp] protected theorem pos_iff {x : R} : 0 < abv x ↔ x ≠ 0 :=
⟨λ h₁, mt abv.eq_zero.mpr h₁.ne', abv.pos⟩

protected theorem ne_zero {x : R} (hx : x ≠ 0) : abv x ≠ 0 := (abv.pos hx).ne'

theorem map_one_of_is_regular (h : is_left_regular (abv 1)) : abv 1 = 1 :=
h $ by simp [←abv.map_mul]

@[simp] protected theorem map_zero : abv 0 = 0 := abv.eq_zero.2 rfl

end semiring

section ring

variables {R S : Type*} [ring R] [ordered_semiring S] (abv : absolute_value R S)

protected lemma sub_le (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c) :=
by simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)

@[simp] lemma map_sub_eq_zero_iff (a b : R) : abv (a - b) = 0 ↔ a = b :=
abv.eq_zero.trans sub_eq_zero

end ring

end ordered_semiring

section ordered_ring

section semiring

section is_domain

-- all of these are true for `no_zero_divisors S`; but it doesn't work smoothly with the
-- `is_domain`/`cancel_monoid_with_zero` API
variables {R S : Type*} [semiring R] [ordered_ring S] (abv : absolute_value R S)
variables [is_domain S] [nontrivial R]

@[simp] protected theorem map_one : abv 1 = 1 :=
abv.map_one_of_is_regular ((is_regular_of_ne_zero $ abv.ne_zero one_ne_zero).left)

instance : monoid_with_zero_hom_class (absolute_value R S) R S :=
{ map_zero := λ f, f.map_zero,
  map_one := λ f, f.map_one,
  ..absolute_value.mul_hom_class }

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*`, `0` and `1`. -/
def to_monoid_with_zero_hom : R →*₀ S := abv

@[simp] lemma coe_to_monoid_with_zero_hom : ⇑abv.to_monoid_with_zero_hom = abv := rfl

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*` and `1`. -/
def to_monoid_hom : R →* S := abv

@[simp] lemma coe_to_monoid_hom : ⇑abv.to_monoid_hom = abv := rfl

@[simp] protected lemma map_pow (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
abv.to_monoid_hom.map_pow a n

end is_domain

end semiring

section ring

variables {R S : Type*} [ring R] [ordered_ring S] (abv : absolute_value R S)

protected lemma le_sub (a b : R) : abv a - abv b ≤ abv (a - b) :=
sub_le_iff_le_add.2 $ by simpa using abv.add_le (a - b) b

end ring

end ordered_ring

section ordered_comm_ring

variables {R S : Type*} [ring R] [ordered_comm_ring S] (abv : absolute_value R S)
variables [no_zero_divisors S]

@[simp] protected theorem map_neg (a : R) : abv (-a) = abv a :=
begin
  by_cases ha : a = 0, { simp [ha] },
  refine (mul_self_eq_mul_self_iff.mp
    (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right _,
  exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'
end

protected theorem map_sub (a b : R) : abv (a - b) = abv (b - a) :=
by rw [← neg_sub, abv.map_neg]

end ordered_comm_ring

instance {R S : Type*} [ring R] [ordered_comm_ring S] [nontrivial R] [is_domain S] :
  mul_ring_norm_class (absolute_value R S) R S :=
{ map_neg_eq_map := λ f, f.map_neg,
  eq_zero_of_map_eq_zero := λ f a, f.eq_zero.1,
  ..absolute_value.subadditive_hom_class, ..absolute_value.monoid_with_zero_hom_class }

section linear_ordered_ring

variables {R S : Type*} [semiring R] [linear_ordered_ring S] (abv : absolute_value R S)

/-- `absolute_value.abs` is `abs` as a bundled `absolute_value`. -/
@[simps]
protected def abs : absolute_value S S :=
{ to_fun := abs,
  nonneg' := abs_nonneg,
  eq_zero' := λ _, abs_eq_zero,
  add_le' := abs_add,
  map_mul' := abs_mul }

instance : inhabited (absolute_value S S) := ⟨absolute_value.abs⟩

end linear_ordered_ring

section linear_ordered_comm_ring

variables {R S : Type*} [ring R] [linear_ordered_comm_ring S] (abv : absolute_value R S)

lemma abs_abv_sub_le_abv_sub (a b : R) :
  abs (abv a - abv b) ≤ abv (a - b) :=
abs_sub_le_iff.2 ⟨abv.le_sub _ _, by rw abv.map_sub; apply abv.le_sub⟩

end linear_ordered_comm_ring

end absolute_value

/-- A function `f` is an absolute value if it is nonnegative, zero only at 0, additive, and
multiplicative.

See also the type `absolute_value` which represents a bundled version of absolute values.
-/
class is_absolute_value {S} [ordered_semiring S]
  {R} [semiring R] (f : R → S) : Prop :=
(abv_nonneg [] : ∀ x, 0 ≤ f x)
(abv_eq_zero [] : ∀ {x}, f x = 0 ↔ x = 0)
(abv_add [] : ∀ x y, f (x + y) ≤ f x + f y)
(abv_mul [] : ∀ x y, f (x * y) = f x * f y)

namespace is_absolute_value

section ordered_semiring

variables {S : Type*} [ordered_semiring S]
variables {R : Type*} [semiring R] (abv : R → S) [is_absolute_value abv]

/-- A bundled absolute value is an absolute value. -/
instance _root_.absolute_value.is_absolute_value
  (abv : absolute_value R S) : is_absolute_value abv :=
{ abv_nonneg := abv.nonneg,
  abv_eq_zero := λ _, abv.eq_zero,
  abv_add := abv.add_le,
  abv_mul := abv.map_mul }

/-- Convert an unbundled `is_absolute_value` to a bundled `absolute_value`. -/
@[simps]
def to_absolute_value : absolute_value R S :=
{ to_fun := abv,
  add_le' := abv_add abv,
  eq_zero' := λ _, abv_eq_zero abv,
  nonneg' := abv_nonneg abv,
  map_mul' := abv_mul abv }

theorem abv_zero : abv 0 = 0 := (to_absolute_value abv).map_zero

theorem abv_pos {a : R} : 0 < abv a ↔ a ≠ 0 := (to_absolute_value abv).pos_iff

end ordered_semiring

section linear_ordered_ring

variables {S : Type*} [linear_ordered_ring S]

instance abs_is_absolute_value : is_absolute_value (abs : S → S) :=
  absolute_value.abs.is_absolute_value

end linear_ordered_ring

section ordered_ring

variables {S : Type*} [ordered_ring S]

section semiring

variables {R : Type*} [semiring R] (abv : R → S) [is_absolute_value abv]

variables [is_domain S]

theorem abv_one [nontrivial R] : abv 1 = 1 := (to_absolute_value abv).map_one

/-- `abv` as a `monoid_with_zero_hom`. -/
def abv_hom [nontrivial R] : R →*₀ S := (to_absolute_value abv).to_monoid_with_zero_hom

lemma abv_pow [nontrivial R] (abv : R → S) [is_absolute_value abv]
  (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
(to_absolute_value abv).map_pow a n

end semiring

section ring

variables {R : Type*} [ring R] (abv : R → S) [is_absolute_value abv]

lemma abv_sub_le (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c) :=
by simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)

lemma sub_abv_le_abv_sub (a b : R) : abv a - abv b ≤ abv (a - b) :=
(to_absolute_value abv).le_sub a b

end ring

end ordered_ring

section ordered_comm_ring

variables {S : Type*} [ordered_comm_ring S]

section ring

variables {R : Type*} [ring R] (abv : R → S) [is_absolute_value abv]

variables [no_zero_divisors S]

theorem abv_neg (a : R) : abv (-a) = abv a :=
(to_absolute_value abv).map_neg a

end ring

end ordered_comm_ring

section linear_ordered_comm_ring

variables {S : Type*} [linear_ordered_comm_ring S]

section ring

variables {R : Type*} [ring R] (abv : R → S) [is_absolute_value abv]

lemma abs_abv_sub_le_abv_sub (a b : R) :
  abs (abv a - abv b) ≤ abv (a - b) :=
(to_absolute_value abv).abs_abv_sub_le_abv_sub a b

end ring

end linear_ordered_comm_ring

section linear_ordered_field

variables {S : Type*} [linear_ordered_semifield S]

section semiring

variables {R : Type*} [semiring R] [nontrivial R] (abv : R → S) [is_absolute_value abv]

lemma abv_one' : abv 1 = 1 :=
(to_absolute_value abv).map_one_of_is_regular
  $ (is_regular_of_ne_zero $ (to_absolute_value abv).ne_zero one_ne_zero).left

/-- An absolute value as a monoid with zero homomorphism, assuming the target is a semifield. -/
def abv_hom' : R →*₀ S := ⟨abv, abv_zero abv, abv_one' abv, abv_mul abv⟩

end semiring

section division_semiring

variables {R : Type*} [division_semiring R] (abv : R → S) [is_absolute_value abv]

theorem abv_inv (a : R) : abv a⁻¹ = (abv a)⁻¹ := map_inv₀ (abv_hom' abv) a
theorem abv_div (a b : R) : abv (a / b) = abv a / abv b := map_div₀ (abv_hom' abv) a b

end division_semiring

end linear_ordered_field

end is_absolute_value

repo: mathlib


text:
/-
Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ulrik Buchholtz
-/

import ..function
universes u v w
hott_theory
namespace hott

open hott.is_equiv hott.function fiber

namespace arrow

  @[hott] structure arrow :=
    (dom : Type _)
    (cod : Type _)
    (arrow : dom → cod)

  @[hott] def arrow_of_fn {A B : Type _} (f : A → B) : arrow :=
  arrow.mk A B f

  @[hott] instance : has_coe_to_fun arrow :=
  ⟨λf, f.dom → f.cod, arrow.arrow⟩

  -- structure morphism (A B : Type _) :=
  --   (mor : A → B)

  -- @[hott] def morphism_of_arrow (f : arrow) : morphism f.dom f.cod :=
  -- morphism.mk (arrow.arrow f)

  -- attribute [coercion] morphism.mor

  @[hott] structure arrow_hom (f g : arrow) :=
    (on_dom : f.dom → g.dom)
    (on_cod : f.cod → g.cod)
    (commute : Π(x : f.dom), g (on_dom x) = on_cod (f x))

  -- abbreviation on_dom := @arrow_hom.on_dom
  -- abbreviation on_cod := @arrow_hom.on_cod
  -- abbreviation commute := @arrow_hom.commute

  variables {f : arrow} {g : arrow}

  @[hott] def on_fiber (r : arrow_hom f g) (y : f.cod)
    : fiber f y → fiber g (r.on_cod y) :=
  λz, fiber.rec (λx p, fiber.mk (r.on_dom x) (r.commute x ⬝ ap (r.on_cod) p)) z

  @[hott, class] structure is_retraction (r : arrow_hom f g) :=
    (sect : arrow_hom g f)
    (right_inverse_dom : Π(a : g.dom), r.on_dom (sect.on_dom a) = a)
    (right_inverse_cod : Π(b : g.cod), r.on_cod (sect.on_cod b) = b)
    (cohere : Π(a : g.dom), r.commute (sect.on_dom a) ⬝ ap (r.on_cod) (sect.commute a)
                            = ap g (right_inverse_dom a) ⬝ (right_inverse_cod (g a))⁻¹)

  abbreviation arrow_hom.sect := @is_retraction.sect

  @[hott] def retraction_on_fiber (r : arrow_hom f g) [H : is_retraction r]
    (b : g.cod) : fiber f (r.sect.on_cod b) → fiber g b :=
  λz, fiber.rec (λx q, fiber.mk (r.on_dom x) (r.commute x ⬝ ap (r.on_cod) q ⬝ is_retraction.right_inverse_cod r b)) z

  @[hott] def retraction_on_fiber_right_inverse' (r : arrow_hom f g) [H : is_retraction r]
    (a : g.dom) (b : g.cod) (p : g a = b)
    : retraction_on_fiber r b (on_fiber r.sect b (fiber.mk a p)) = fiber.mk a p :=
  begin
    induction p, dsimp [on_fiber, retraction_on_fiber],
    apply @fiber.fiber_eq _ _ g (g a)
      (fiber.mk
        (r.on_dom (r.sect.on_dom a))
        (r.commute (r.sect.on_dom a)
          ⬝ ap (r.on_cod) (r.sect.commute a)
          ⬝ is_retraction.right_inverse_cod r (g a)))
      (fiber.mk a (refl (g a)))
      (is_retraction.right_inverse_dom r a), -- everything but this field should be inferred
    rwr [is_retraction.cohere r a],
    apply inv_con_cancel_right
  end

  @[hott] def retraction_on_fiber_right_inverse (r : arrow_hom f g) [H : is_retraction r]
    : Π(b : g.cod), Π(z : fiber g b), retraction_on_fiber r b (on_fiber r.sect b z) = z :=
  λb z, fiber.rec (λa p, retraction_on_fiber_right_inverse' r a b p) z

  -- @[hott] lemma 4.7.3
  @[hott, instance] def retraction_on_fiber_is_retraction (r : arrow_hom f g) [H : is_retraction r]
    (b : g.cod) : hott.is_retraction (retraction_on_fiber r b) :=
  hott.is_retraction.mk (on_fiber r.sect b) (retraction_on_fiber_right_inverse r b)

  -- @[hott] theorem 4.7.4
  @[hott] def retract_of_equivalence_is_equivalence (r : arrow_hom f g) [H : is_retraction r]
    [K : is_equiv f] : is_equiv g :=
  begin
    have : is_contr_fun g, intro b,
      apply is_contr_retract (retraction_on_fiber r b),
      exact is_contr_fun_of_is_equiv f (r.sect.on_cod b),
    exactI is_equiv_of_is_contr_fun g
  end

end arrow

namespace arrow
  variables {A : Type _} {B : Type _} {f g : A → B} (p : f ~ g)

  @[hott] def arrow_hom_of_homotopy : arrow_hom (arrow_of_fn f) (arrow_of_fn g) :=
  arrow_hom.mk id id (λx, (p x)⁻¹)

  @[hott, instance] def is_retraction_arrow_hom_of_homotopy
    : is_retraction (arrow_hom_of_homotopy p) :=
  is_retraction.mk
    (arrow_hom_of_homotopy (λx, (p x)⁻¹))
    (λa, idp)
    (λb, idp)
    (λa, con_eq_of_eq_inv_con (ap_id _))

end arrow

namespace arrow
  /-
    equivalences in the arrow category; could be packaged into structures.
    cannot be moved to types.pi because of the dependence on types.equiv.
  -/

  variables {A : Type _} {A' : Type _} {B : Type _} {B' : Type _} (f : A → B) (f' : A' → B')
            (α : A → A') (β : B → B')
            [Hf : is_equiv f] [Hf' : is_equiv f']
  include Hf Hf'

  open function
  @[hott] def inv_commute_of_commute (p : f' ∘ α ~ β ∘ f) : f'⁻¹ᶠ ∘ β ~ α ∘ f⁻¹ᶠ :=
  begin
    apply inv_homotopy_of_homotopy_post f' (α ∘ f⁻¹ᶠ) β,
    apply homotopy.symm,
    apply inv_homotopy_of_homotopy_pre f (f' ∘ α) β,
    apply p
  end

  @[hott] def inv_commute_of_commute_top (p : f' ∘ α ~ β ∘ f) (a : A)
    : inv_commute_of_commute f f' α β p (f a)
    =  (ap f'⁻¹ᶠ (p a))⁻¹ ⬝ left_inv f' (α a) ⬝ ap α (left_inv f a)⁻¹ :=
  begin
    dsimp [inv_commute_of_commute, inv_homotopy_of_homotopy_post, inv_homotopy_of_homotopy_pre,
           homotopy.symm],
    rwr [adj f a,←ap_compose β f],
    rwr [eq_of_square (natural_square p (left_inv f a))],
    rwr [ap_inv f'⁻¹ᶠ,ap_con f'⁻¹ᶠ,con_inv,con.assoc,con.assoc],
    apply whisker_left (ap f'⁻¹ᶠ (p a))⁻¹,
    apply eq_of_square, rwr [ap_inv α,←(ap_compose f'⁻¹ᶠ (f' ∘ α))],
    apply hinverse, rwr [ap_compose (f'⁻¹ᶠ ∘ f') α],
    refine vconcat_eq _ (ap_id (ap α (left_inv f a))),
    apply natural_square_tr (left_inv f') (ap α (left_inv f a))
  end

  @[hott] def ap_bot_inv_commute_of_commute (p : f' ∘ α ~ β ∘ f) (b : B)
    : ap f' (inv_commute_of_commute f f' α β p b)
    = right_inv f' (β b) ⬝ ap β (right_inv f b)⁻¹ ⬝ (p (f⁻¹ᶠ b))⁻¹ :=
  begin
    dsimp [inv_commute_of_commute, inv_homotopy_of_homotopy_post, inv_homotopy_of_homotopy_pre],
    rwr [ap_con,←(ap_compose f' f'⁻¹ᶠ),←(adj f' (α (f⁻¹ᶠ b)))],
    rwr [con.assoc (right_inv f' (β b)) (ap β (right_inv f b)⁻¹)
                       (p (f⁻¹ᶠ b))⁻¹],
    apply eq_of_square,
    refine vconcat_eq _
      (whisker_right (p (f⁻¹ᶠ b))⁻¹ (ap_inv β (right_inv f b)))⁻¹ᵖ,
    refine vconcat_eq _
      (con_inv (p (f⁻¹ᶠ b)) (ap β (right_inv f b))),
    refine vconcat_eq _
      (ap_id (p (f⁻¹ᶠ b) ⬝ ap β (right_inv f b))⁻¹),
    apply natural_square_tr (right_inv f')
      (p (f⁻¹ᶠ b) ⬝ ap β (right_inv f b))⁻¹
  end

  @[hott] def is_equiv_inv_commute_of_commute
    : is_equiv (inv_commute_of_commute f f' α β) :=
  begin
    delta inv_commute_of_commute,
    napply @is_equiv_compose _ _ _ (inv_homotopy_of_homotopy_post f' (α ∘ f⁻¹ᶠ) β)
      (homotopy.symm ∘ (inv_homotopy_of_homotopy_pre f (f' ∘ α) β)),
    { napply @is_equiv_compose _ _ _ homotopy.symm (inv_homotopy_of_homotopy_pre f (f' ∘ α) β),
      { apply inv_homotopy_of_homotopy_pre.is_equiv },
      { apply pi.is_equiv_homotopy_symm }
    },
    { apply inv_homotopy_of_homotopy_post.is_equiv }
  end
end arrow
end hott

author: gebner


/-
Copyright 2022 Google LLC

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.

Authors: Moritz Firsching
-/
import tactic
import data.real.basic
import data.complex.exponential
import analysis.calculus.iterated_deriv
import analysis.special_functions.trigonometric.basic
import analysis.special_functions.trigonometric.inverse

open real (exp pi arccos)

open finset (Icc)
open_locale big_operators
/-!
# Some irrational numbers

## TODO : All proofs,
## Outline
  - $e$ is irrational
  - $e^2$ is irrational
  - $e^4$ is irrational
  - Lemma
    - (i)
    - (ii)
    - (iii)
    - proof
      - (i)
      - (ii)
      - (iii)
  - Theorem 1.
    - proof
  - Theorem 2.
    - proof
  - Theorem 3.
    - proof
-/

namespace book
namespace irrational

/-- A real number is irrational if it is not rational. This is the same definition as in mathlib -/
def irrational (x : ℝ) := x ∉ set.range (coe : ℚ → ℝ)

/-- This is `irrational_iff_ne_rational` in mathlib. -/
lemma irrational_iff_not_fraction (x : ℝ) : irrational x ↔ ∀ a b : ℤ, x ≠ (a : ℝ) / b :=
begin
  sorry,
end

/-- We define abbreviations for Euler's and for Pi-/
noncomputable def e := exp 1
noncomputable def π := pi

/-- We want to use the series representation of the exponential function-/
theorem exponential_series (x : ℝ) : has_sum (λ n : ℕ, x ^ n / (n.factorial)) (real.exp x) :=
begin
  sorry,
end

/-!
## Some Proofs of irrationality
-/

theorem e_irrational : irrational e :=
begin
  sorry,
end

theorem e_pow_2_irrational : irrational (e ^ 2) :=
begin
  sorry,
end

/--
"For any `n ≥ 1` the integer `n!` contains the prime factor `2` at most `n − 1` times —
with equality if (and only if) `n` is a power of two, `n = 2 ^ m`."
-/
lemma little_lemma (n : ℕ) (h_n : n ≠ 0) :
  ¬ (2 ^ n ∣ n.factorial) ∧ (2 ^ (n - 1) ∣ n.factorial ↔ ∃ m : ℕ, n = 2 ^ m) :=
begin
  sorry,
end

theorem e_pow_4_irrational : irrational (e ^ 4) :=
begin
  sorry,
end

/-!  ### Proofs of the main theorems-/

/-!
####  Auxiliary Lemma
We first prove the following lemma (see `lem_aux_i` to `lem_aux_iii` below):
Let `n : ℕ`, `n ≥ 1` be fixed, and consider `f_aux n x = x ^ n * (1 - x) ^ n / n.factorial`. Then
(i) `f_aux n` is equal, as a function in `x`, to a polynomial of the form
  `(sum (i : Icc n (2 * n)), (c i) x ^i) / n.factorial`, where `c i : ℤ`.
(ii) For `0 < x < 1` we have `0 < f_aux n x < 1 / n.factorial` .
(iii) The `k`-th derivatives `iterated_deriv k (f_aux n)` take integer values at `x = 0` and `x = 1`
   for all `k ≥ 0`.
-/

noncomputable def f_aux (n : ℕ) (x : ℝ) :=  x ^ n * (1 - x) ^ n / n.factorial

lemma lem_aux_i (n : ℕ) (x : ℝ) : ∃ c : ℕ → ℤ, f_aux n x = ∑ i in Icc n (2 * n), (c i) * x ^ i :=
begin
  sorry,
end

lemma lem_aux_ii (n : ℕ) (x : ℝ) (h_1 : 0 < x) (h_2 x < 0) :
  (0 < f_aux n x) ∧ (f_aux n x < (1 : ℝ) / n.factorial) :=
begin
  sorry,
end

/--
WARNING: There might be a better way to state this, not sure what the best API for derivatives of
smooth (polynomial) functions is
-/
lemma lem_aux_iii (n : ℕ) (k : ℕ): iterated_deriv k (f_aux n) 0 ∈  set.range (coe : ℚ → ℝ) ∧
  iterated_deriv k (f_aux n) 1 ∈ set.range (coe : ℚ → ℝ) :=
begin
  sorry,
end

/-! ### Theorems 1 to 3 -/

/--For any non-zero rational number `r`, the exponential `e ^ r` is irrational.-/
theorem Theorem_1 (r : ℚ) (h_r : r ≠ 0) : irrational (exp r) :=
begin
  suffices : ∀ k : ℤ, k > 0 → irrational (exp k), by
  begin
    sorry,
  end,
  sorry,
end

theorem Theorem_2 (r : ℚ) (h_r : r ≠ 0) : irrational (π ^ 2) :=
begin
  sorry,
end

theorem Theorem_3 (n : ℕ) (h_n : n ≥ 3) : irrational ( arccos (1 / (n : ℝ).sqrt) / π) :=
begin
  sorry,
end

end irrational
end book


text:
/-
Copyright (c) 2022 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser

! This file was ported from Lean 3 source module data.mv_polynomial.division
! leanprover-community/mathlib commit 72c366d0475675f1309d3027d3d7d47ee4423951
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.MonoidAlgebra.Division
import Mathlib.Data.MvPolynomial.Basic

/-!
# Division of `MvPolynomial` by monomials

## Main definitions

* `MvPolynomial.divMonomial x s`: divides `x` by the monomial `MvPolynomial.monomial 1 s`
* `MvPolynomial.modMonomial x s`: the remainder upon dividing `x` by the monomial
  `MvPolynomial.monomial 1 s`.

## Main results

* `MvPolynomial.divMonomial_add_modMonomial`, `MvPolynomial.modMonomial_add_divMonomial`:
  `divMonomial` and `modMonomial` are well-behaved as quotient and remainder operators.

## Implementation notes

Where possible, the results in this file should be first proved in the generality of
`AddMonoidAlgebra`, and then the versions specialized to `MvPolynomial` proved in terms of these.

-/

variable {σ R : Type _} [CommSemiring R]

namespace MvPolynomial

section CopiedDeclarations

/-! Please ensure the declarations in this section are direct translations of `AddMonoidAlgebra`
results. -/

/-- Divide by `monomial 1 s`, discarding terms not divisible by this. -/
noncomputable def divMonomial (p : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial σ R :=
  AddMonoidAlgebra.divOf p s
#align mv_polynomial.div_monomial MvPolynomial.divMonomial

local infixl:70 " /ᵐᵒⁿᵒᵐⁱᵃˡ " => divMonomial

@[simp]
theorem coeff_divMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) (s' : σ →₀ ℕ) :
    coeff s' (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) = coeff (s + s') x :=
  rfl
#align mv_polynomial.coeff_div_monomial MvPolynomial.coeff_divMonomial

@[simp]
theorem support_divMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) :
    (x /ᵐᵒⁿᵒᵐⁱᵃˡ s).support = x.support.preimage _ ((add_right_injective s).injOn _) :=
  rfl
#align mv_polynomial.support_div_monomial MvPolynomial.support_divMonomial

@[simp]
theorem zero_divMonomial (s : σ →₀ ℕ) : (0 : MvPolynomial σ R) /ᵐᵒⁿᵒᵐⁱᵃˡ s = 0 :=
  AddMonoidAlgebra.zero_divOf _
#align mv_polynomial.zero_div_monomial MvPolynomial.zero_divMonomial

theorem divMonomial_zero (x : MvPolynomial σ R) : x /ᵐᵒⁿᵒᵐⁱᵃˡ 0 = x :=
  x.divOf_zero
#align mv_polynomial.div_monomial_zero MvPolynomial.divMonomial_zero

theorem add_divMonomial (x y : MvPolynomial σ R) (s : σ →₀ ℕ) :
    (x + y) /ᵐᵒⁿᵒᵐⁱᵃˡ s = x /ᵐᵒⁿᵒᵐⁱᵃˡ s + y /ᵐᵒⁿᵒᵐⁱᵃˡ s :=
  map_add _ _ _
#align mv_polynomial.add_div_monomial MvPolynomial.add_divMonomial

theorem divMonomial_add (a b : σ →₀ ℕ) (x : MvPolynomial σ R) :
    x /ᵐᵒⁿᵒᵐⁱᵃˡ (a + b) = x /ᵐᵒⁿᵒᵐⁱᵃˡ a /ᵐᵒⁿᵒᵐⁱᵃˡ b :=
  x.divOf_add _ _
#align mv_polynomial.div_monomial_add MvPolynomial.divMonomial_add

@[simp]
theorem divMonomial_monomial_mul (a : σ →₀ ℕ) (x : MvPolynomial σ R) :
    monomial a 1 * x /ᵐᵒⁿᵒᵐⁱᵃˡ a = x :=
  x.of'_mul_divOf _
#align mv_polynomial.div_monomial_monomial_mul MvPolynomial.divMonomial_monomial_mul

@[simp]
theorem divMonomial_mul_monomial (a : σ →₀ ℕ) (x : MvPolynomial σ R) :
    x * monomial a 1 /ᵐᵒⁿᵒᵐⁱᵃˡ a = x :=
  x.mul_of'_divOf _
#align mv_polynomial.div_monomial_mul_monomial MvPolynomial.divMonomial_mul_monomial

@[simp]
theorem divMonomial_monomial (a : σ →₀ ℕ) : monomial a 1 /ᵐᵒⁿᵒᵐⁱᵃˡ a = (1 : MvPolynomial σ R) :=
  AddMonoidAlgebra.of'_divOf _
#align mv_polynomial.div_monomial_monomial MvPolynomial.divMonomial_monomial

/-- The remainder upon division by `monomial 1 s`. -/
noncomputable def modMonomial (x : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial σ R :=
  x.modOf s
#align mv_polynomial.mod_monomial MvPolynomial.modMonomial

local infixl:70 " %ᵐᵒⁿᵒᵐⁱᵃˡ " => modMonomial

@[simp]
theorem coeff_modMonomial_of_not_le {s' s : σ →₀ ℕ} (x : MvPolynomial σ R) (h : ¬s ≤ s') :
    coeff s' (x %ᵐᵒⁿᵒᵐⁱᵃˡ s) = coeff s' x :=
  x.modOf_apply_of_not_exists_add s s'
    (by
      rintro ⟨d, rfl⟩
      exact h le_self_add)
#align mv_polynomial.coeff_mod_monomial_of_not_le MvPolynomial.coeff_modMonomial_of_not_le

@[simp]
theorem coeff_modMonomial_of_le {s' s : σ →₀ ℕ} (x : MvPolynomial σ R) (h : s ≤ s') :
    coeff s' (x %ᵐᵒⁿᵒᵐⁱᵃˡ s) = 0 :=
  x.modOf_apply_of_exists_add _ _ <| exists_add_of_le h
#align mv_polynomial.coeff_mod_monomial_of_le MvPolynomial.coeff_modMonomial_of_le

@[simp]
theorem monomial_mul_modMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) :
    monomial s 1 * x %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0 :=
  x.of'_mul_modOf _
#align mv_polynomial.monomial_mul_mod_monomial MvPolynomial.monomial_mul_modMonomial

@[simp]
theorem mul_monomial_modMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) :
    x * monomial s 1 %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0 :=
  x.mul_of'_modOf _
#align mv_polynomial.mul_monomial_mod_monomial MvPolynomial.mul_monomial_modMonomial

@[simp]
theorem monomial_modMonomial (s : σ →₀ ℕ) : monomial s (1 : R) %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0 :=
  AddMonoidAlgebra.of'_modOf _
#align mv_polynomial.monomial_mod_monomial MvPolynomial.monomial_modMonomial

theorem divMonomial_add_modMonomial (x : MvPolynomial σ R) (s : σ →₀ ℕ) :
    monomial s 1 * (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) + x %ᵐᵒⁿᵒᵐⁱᵃˡ s = x :=
  AddMonoidAlgebra.divOf_add_modOf x s
#align mv_polynomial.div_monomial_add_mod_monomial MvPolynomial.divMonomial_add_modMonomial

theorem modMonomial_add_divMonomial (x : MvPolynomial σ R) (s : σ →₀ ℕ) :
    x %ᵐᵒⁿᵒᵐⁱᵃˡ s + monomial s 1 * (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) = x :=
  AddMonoidAlgebra.modOf_add_divOf x s
#align mv_polynomial.mod_monomial_add_div_monomial MvPolynomial.modMonomial_add_divMonomial

theorem monomial_one_dvd_iff_modMonomial_eq_zero {i : σ →₀ ℕ} {x : MvPolynomial σ R} :
    monomial i (1 : R) ∣ x ↔ x %ᵐᵒⁿᵒᵐⁱᵃˡ i = 0 :=
  AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero
#align mv_polynomial.monomial_one_dvd_iff_mod_monomial_eq_zero MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero

end CopiedDeclarations

section XLemmas

local infixl:70 " /ᵐᵒⁿᵒᵐⁱᵃˡ " => divMonomial

local infixl:70 " %ᵐᵒⁿᵒᵐⁱᵃˡ " => modMonomial

@[simp]
theorem x_mul_divMonomial (i : σ) (x : MvPolynomial σ R) :
    X i * x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x :=
  divMonomial_monomial_mul _ _
set_option linter.uppercaseLean3 false in
#align mv_polynomial.X_mul_div_monomial MvPolynomial.x_mul_divMonomial

@[simp]
theorem x_divMonomial (i : σ) : (X i : MvPolynomial σ R) /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 1 :=
  divMonomial_monomial (Finsupp.single i 1)
set_option linter.uppercaseLean3 false in
#align mv_polynomial.X_div_monomial MvPolynomial.x_divMonomial

@[simp]
theorem mul_x_divMonomial (x : MvPolynomial σ R) (i : σ) :
    x * X i /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x :=
  divMonomial_mul_monomial _ _
set_option linter.uppercaseLean3 false in
#align mv_polynomial.mul_X_div_monomial MvPolynomial.mul_x_divMonomial

@[simp]
theorem x_mul_modMonomial (i : σ) (x : MvPolynomial σ R) :
    X i * x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
  monomial_mul_modMonomial _ _
set_option linter.uppercaseLean3 false in
#align mv_polynomial.X_mul_mod_monomial MvPolynomial.x_mul_modMonomial

@[simp]
theorem mul_x_modMonomial (x : MvPolynomial σ R) (i : σ) :
    x * X i %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
  mul_monomial_modMonomial _ _
set_option linter.uppercaseLean3 false in
#align mv_polynomial.mul_X_mod_monomial MvPolynomial.mul_x_modMonomial

@[simp]
theorem modMonomial_x (i : σ) : (X i : MvPolynomial σ R) %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
  monomial_modMonomial _
set_option linter.uppercaseLean3 false in
#align mv_polynomial.mod_monomial_X MvPolynomial.modMonomial_x

theorem divMonomial_add_modMonomial_single (x : MvPolynomial σ R) (i : σ) :
    X i * (x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) + x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x :=
  divMonomial_add_modMonomial _ _
#align mv_polynomial.div_monomial_add_mod_monomial_single MvPolynomial.divMonomial_add_modMonomial_single

theorem modMonomial_add_divMonomial_single (x : MvPolynomial σ R) (i : σ) :
    x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 + X i * (x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) = x :=
  modMonomial_add_divMonomial _ _
#align mv_polynomial.mod_monomial_add_div_monomial_single MvPolynomial.modMonomial_add_divMonomial_single

theorem x_dvd_iff_modMonomial_eq_zero {i : σ} {x : MvPolynomial σ R} :
    X i ∣ x ↔ x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
  monomial_one_dvd_iff_modMonomial_eq_zero
set_option linter.uppercaseLean3 false in
#align mv_polynomial.X_dvd_iff_mod_monomial_eq_zero MvPolynomial.x_dvd_iff_modMonomial_eq_zero

end XLemmas

/-! ### Some results about dvd (`∣`) on `monomial` and `X` -/

theorem monomial_dvd_monomial {r s : R} {i j : σ →₀ ℕ} :
    monomial i r ∣ monomial j s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s := by
  constructor
  · rintro ⟨x, hx⟩
    rw [MvPolynomial.ext_iff] at hx
    have hj := hx j
    have hi := hx i
    classical
      simp_rw [coeff_monomial, if_pos] at hj hi
      simp_rw [coeff_monomial_mul', if_pos] at hi hj
      split_ifs  at hi hj with hi hi
      · exact ⟨Or.inr hi, _, hj⟩
      · exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
    -- Porting note: two goals remain at this point in Lean 4
    · simp_all only [or_true, dvd_mul_right]
    · simp_all only [ite_self, le_refl, ite_true, dvd_mul_right]
  · rintro ⟨h | hij, d, rfl⟩
    · simp_rw [h, monomial_zero, dvd_zero]
    · refine' ⟨monomial (j - i) d, _⟩
      rw [monomial_mul, add_tsub_cancel_of_le hij]
#align mv_polynomial.monomial_dvd_monomial MvPolynomial.monomial_dvd_monomial

@[simp]
theorem monomial_one_dvd_monomial_one [Nontrivial R] {i j : σ →₀ ℕ} :
    monomial i (1 : R) ∣ monomial j 1 ↔ i ≤ j := by
  rw [monomial_dvd_monomial]
  simp_rw [one_ne_zero, false_or_iff, dvd_rfl, and_true_iff]
#align mv_polynomial.monomial_one_dvd_monomial_one MvPolynomial.monomial_one_dvd_monomial_one

@[simp]
theorem x_dvd_x [Nontrivial R] {i j : σ} :
    (X i : MvPolynomial σ R) ∣ (X j : MvPolynomial σ R) ↔ i = j := by
  refine' monomial_one_dvd_monomial_one.trans _
  simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero, Ne.def,
    one_ne_zero, not_false_iff, and_true_iff]
set_option linter.uppercaseLean3 false in
#align mv_polynomial.X_dvd_X MvPolynomial.x_dvd_x

@[simp]
theorem x_dvd_monomial {i : σ} {j : σ →₀ ℕ} {r : R} :
    (X i : MvPolynomial σ R) ∣ monomial j r ↔ r = 0 ∨ j i ≠ 0 := by
  refine' monomial_dvd_monomial.trans _
  simp_rw [one_dvd, and_true_iff, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
set_option linter.uppercaseLean3 false in
#align mv_polynomial.X_dvd_monomial MvPolynomial.x_dvd_monomial

end MvPolynomial