text:
/-
Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel

! This file was ported from Lean 3 source module analysis.calculus.series
! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Analysis.Calculus.UniformLimitsDeriv
import Mathbin.Analysis.Calculus.ContDiff
import Mathbin.Data.Nat.Cast.WithTop

/-!
# Smoothness of series

We show that series of functions are continuous, or differentiable, or smooth, when each individual
function in the series is and additionally suitable uniform summable bounds are satisfied.

More specifically,
* `continuous_tsum` ensures that a series of continuous functions is continuous.
* `differentiable_tsum` ensures that a series of differentiable functions is differentiable.
* `cont_diff_tsum` ensures that a series of smooth functions is smooth.

We also give versions of these statements which are localized to a set.
-/

open Set Metric TopologicalSpace Function Asymptotics Filter

open Topology NNReal BigOperators

variable {α β 𝕜 E F : Type _} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}

/-! ### Continuity -/

/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version relative to a set, with general index set. -/
theorem tendstoUniformlyOn_tsum {f : α → β → F} (hu : Summable u) {s : Set β}
    (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) :
    TendstoUniformlyOn (fun t : Finset α => fun x => ∑ n in t, f n x) (fun x => ∑' n, f n x) atTop
      s :=
  by
  refine' tendsto_uniformly_on_iff.2 fun ε εpos => _
  filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos]with t ht x hx
  have A : Summable fun n => ‖f n x‖ :=
    summable_of_nonneg_of_le (fun n => norm_nonneg _) (fun n => hfu n x hx) hu
  rw [dist_eq_norm, ← sum_add_tsum_subtype_compl (summable_of_summable_norm A) t, add_sub_cancel']
  apply lt_of_le_of_lt _ ht
  apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
  exact tsum_le_tsum (fun n => hfu _ _ hx) (A.subtype _) (hu.subtype _)
#align tendsto_uniformly_on_tsum tendstoUniformlyOn_tsum

/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version relative to a set, with index set `ℕ`. -/
theorem tendstoUniformlyOn_tsum_nat {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) {s : Set β}
    (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) :
    TendstoUniformlyOn (fun N => fun x => ∑ n in Finset.range N, f n x) (fun x => ∑' n, f n x) atTop
      s :=
  fun v hv => tendsto_finset_range.Eventually (tendstoUniformlyOn_tsum hu hfu v hv)
#align tendsto_uniformly_on_tsum_nat tendstoUniformlyOn_tsum_nat

/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version with general index set. -/
theorem tendstoUniformly_tsum {f : α → β → F} (hu : Summable u) (hfu : ∀ n x, ‖f n x‖ ≤ u n) :
    TendstoUniformly (fun t : Finset α => fun x => ∑ n in t, f n x) (fun x => ∑' n, f n x) atTop :=
  by
  rw [← tendstoUniformlyOn_univ]
  exact tendstoUniformlyOn_tsum hu fun n x hx => hfu n x
#align tendsto_uniformly_tsum tendstoUniformly_tsum

/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version with index set `ℕ`. -/
theorem tendstoUniformly_tsum_nat {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u)
    (hfu : ∀ n x, ‖f n x‖ ≤ u n) :
    TendstoUniformly (fun N => fun x => ∑ n in Finset.range N, f n x) (fun x => ∑' n, f n x)
      atTop :=
  fun v hv => tendsto_finset_range.Eventually (tendstoUniformly_tsum hu hfu v hv)
#align tendsto_uniformly_tsum_nat tendstoUniformly_tsum_nat

/-- An infinite sum of functions with summable sup norm is continuous on a set if each individual
function is. -/
theorem continuousOn_tsum [TopologicalSpace β] {f : α → β → F} {s : Set β}
    (hf : ∀ i, ContinuousOn (f i) s) (hu : Summable u) (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) :
    ContinuousOn (fun x => ∑' n, f n x) s := by
  classical
    refine' (tendstoUniformlyOn_tsum hu hfu).ContinuousOn (eventually_of_forall _)
    intro t
    exact continuousOn_finset_sum _ fun i hi => hf i
#align continuous_on_tsum continuousOn_tsum

/-- An infinite sum of functions with summable sup norm is continuous if each individual
function is. -/
theorem continuous_tsum [TopologicalSpace β] {f : α → β → F} (hf : ∀ i, Continuous (f i))
    (hu : Summable u) (hfu : ∀ n x, ‖f n x‖ ≤ u n) : Continuous fun x => ∑' n, f n x :=
  by
  simp_rw [continuous_iff_continuousOn_univ] at hf⊢
  exact continuousOn_tsum hf hu fun n x hx => hfu n x
#align continuous_tsum continuous_tsum

/-! ### Differentiability -/

variable [NormedSpace 𝕜 F]

variable {f : α → E → F} {f' : α → E → E →L[𝕜] F} {v : ℕ → α → ℝ} {s : Set E} {x₀ x : E} {N : ℕ∞}

/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
at a point, and all functions in the series are differentiable with a summable bound on the
derivatives, then the series converges everywhere on the set. -/
theorem summable_of_summable_hasFderivAt_of_isPreconnected (hu : Summable u) (hs : IsOpen s)
    (h's : IsPreconnected s) (hf : ∀ n x, x ∈ s → HasFderivAt (f n) (f' n x) x)
    (hf' : ∀ n x, x ∈ s → ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable fun n => f n x₀) {x : E}
    (hx : x ∈ s) : Summable fun n => f n x :=
  by
  rw [summable_iff_cauchySeq_finset] at hf0⊢
  have A : UniformCauchySeqOn (fun t : Finset α => fun x => ∑ i in t, f' i x) at_top s :=
    (tendstoUniformlyOn_tsum hu hf').UniformCauchySeqOn
  apply cauchy_map_of_uniformCauchySeqOn_fderiv hs h's A (fun t y hy => _) hx₀ hx hf0
  exact HasFderivAt.sum fun i hi => hf i y hy
#align summable_of_summable_has_fderiv_at_of_is_preconnected summable_of_summable_hasFderivAt_of_isPreconnected

/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
at a point, and all functions in the series are differentiable with a summable bound on the
derivatives, then the series is differentiable on the set and its derivative is the sum of the
derivatives. -/
theorem hasFderivAt_tsum_of_isPreconnected (hu : Summable u) (hs : IsOpen s)
    (h's : IsPreconnected s) (hf : ∀ n x, x ∈ s → HasFderivAt (f n) (f' n x) x)
    (hf' : ∀ n x, x ∈ s → ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable fun n => f n x₀)
    (hx : x ∈ s) : HasFderivAt (fun y => ∑' n, f n y) (∑' n, f' n x) x := by
  classical
    have A :
      ∀ x : E, x ∈ s → tendsto (fun t : Finset α => ∑ n in t, f n x) at_top (𝓝 (∑' n, f n x)) :=
      by
      intro y hy
      apply Summable.hasSum
      exact summable_of_summable_hasFderivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy
    apply
      hasFderivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf') (fun t y hy => _) A _ hx
    exact HasFderivAt.sum fun n hn => hf n y hy
#align has_fderiv_at_tsum_of_is_preconnected hasFderivAt_tsum_of_isPreconnected

/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
point, and all functions in the series are differentiable with a summable bound on the derivatives,
then the series converges everywhere. -/
theorem summable_of_summable_hasFderivAt (hu : Summable u)
    (hf : ∀ n x, HasFderivAt (f n) (f' n x) x) (hf' : ∀ n x, ‖f' n x‖ ≤ u n)
    (hf0 : Summable fun n => f n x₀) (x : E) : Summable fun n => f n x :=
  by
  let : NormedSpace ℝ E; exact NormedSpace.restrictScalars ℝ 𝕜 _
  apply
    summable_of_summable_hasFderivAt_of_isPreconnected hu isOpen_univ
      is_connected_univ.is_preconnected (fun n x hx => hf n x) (fun n x hx => hf' n x) (mem_univ _)
      hf0 (mem_univ _)
#align summable_of_summable_has_fderiv_at summable_of_summable_hasFderivAt

/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
point, and all functions in the series are differentiable with a summable bound on the derivatives,
then the series is differentiable and its derivative is the sum of the derivatives. -/
theorem hasFderivAt_tsum (hu : Summable u) (hf : ∀ n x, HasFderivAt (f n) (f' n x) x)
    (hf' : ∀ n x, ‖f' n x‖ ≤ u n) (hf0 : Summable fun n => f n x₀) (x : E) :
    HasFderivAt (fun y => ∑' n, f n y) (∑' n, f' n x) x :=
  by
  let : NormedSpace ℝ E; exact NormedSpace.restrictScalars ℝ 𝕜 _
  exact
    hasFderivAt_tsum_of_isPreconnected hu isOpen_univ is_connected_univ.is_preconnected
      (fun n x hx => hf n x) (fun n x hx => hf' n x) (mem_univ _) hf0 (mem_univ _)
#align has_fderiv_at_tsum hasFderivAt_tsum

/-- Consider a series of functions `∑' n, f n x`. If all functions in the series are differentiable
with a summable bound on the derivatives, then the series is differentiable.
Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise
convergence then the series is zero everywhere so the result still holds. -/
theorem differentiable_tsum (hu : Summable u) (hf : ∀ n x, HasFderivAt (f n) (f' n x) x)
    (hf' : ∀ n x, ‖f' n x‖ ≤ u n) : Differentiable 𝕜 fun y => ∑' n, f n y :=
  by
  by_cases h : ∃ x₀, Summable fun n => f n x₀
  · rcases h with ⟨x₀, hf0⟩
    intro x
    exact (hasFderivAt_tsum hu hf hf' hf0 x).DifferentiableAt
  · push_neg  at h
    have : (fun x => ∑' n, f n x) = 0 := by
      ext1 x
      exact tsum_eq_zero_of_not_summable (h x)
    rw [this]
    exact differentiable_const 0
#align differentiable_tsum differentiable_tsum

theorem fderiv_tsum_apply (hu : Summable u) (hf : ∀ n, Differentiable 𝕜 (f n))
    (hf' : ∀ n x, ‖fderiv 𝕜 (f n) x‖ ≤ u n) (hf0 : Summable fun n => f n x₀) (x : E) :
    fderiv 𝕜 (fun y => ∑' n, f n y) x = ∑' n, fderiv 𝕜 (f n) x :=
  (hasFderivAt_tsum hu (fun n x => (hf n x).HasFderivAt) hf' hf0 _).fderiv
#align fderiv_tsum_apply fderiv_tsum_apply

theorem fderiv_tsum (hu : Summable u) (hf : ∀ n, Differentiable 𝕜 (f n))
    (hf' : ∀ n x, ‖fderiv 𝕜 (f n) x‖ ≤ u n) {x₀ : E} (hf0 : Summable fun n => f n x₀) :
    (fderiv 𝕜 fun y => ∑' n, f n y) = fun x => ∑' n, fderiv 𝕜 (f n) x :=
  by
  ext1 x
  exact fderiv_tsum_apply hu hf hf' hf0 x
#align fderiv_tsum fderiv_tsum

/-! ### Higher smoothness -/

/-- Consider a series of smooth functions, with summable uniform bounds on the successive
derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative. -/
theorem iteratedFderiv_tsum (hf : ∀ i, ContDiff 𝕜 N (f i))
    (hv : ∀ k : ℕ, (k : ℕ∞) ≤ N → Summable (v k))
    (h'f : ∀ (k : ℕ) (i : α) (x : E), (k : ℕ∞) ≤ N → ‖iteratedFderiv 𝕜 k (f i) x‖ ≤ v k i) {k : ℕ}
    (hk : (k : ℕ∞) ≤ N) :
    (iteratedFderiv 𝕜 k fun y => ∑' n, f n y) = fun x => ∑' n, iteratedFderiv 𝕜 k (f n) x :=
  by
  induction' k with k IH
  · ext1 x
    simp_rw [iteratedFderiv_zero_eq_comp]
    exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum
  · have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
    have A : Summable fun n => iteratedFderiv 𝕜 k (f n) 0 :=
      summable_of_norm_bounded (v k) (hv k h'k.le) fun n => h'f k n 0 h'k.le
    simp_rw [iteratedFderiv_succ_eq_comp_left, IH h'k.le]
    rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFderiv h'k) _ A]
    · ext1 x
      exact
        (continuousMultilinearCurryLeftEquiv 𝕜 (fun i : Fin (k + 1) => E)
              F).toContinuousLinearEquiv.map_tsum
    · intro n x
      simpa only [iteratedFderiv_succ_eq_comp_left, LinearIsometryEquiv.norm_map] using
        h'f k.succ n x hk
#align iterated_fderiv_tsum iteratedFderiv_tsum

/-- Consider a series of smooth functions, with summable uniform bounds on the successive
derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative. -/
theorem iteratedFderiv_tsum_apply (hf : ∀ i, ContDiff 𝕜 N (f i))
    (hv : ∀ k : ℕ, (k : ℕ∞) ≤ N → Summable (v k))
    (h'f : ∀ (k : ℕ) (i : α) (x : E), (k : ℕ∞) ≤ N → ‖iteratedFderiv 𝕜 k (f i) x‖ ≤ v k i) {k : ℕ}
    (hk : (k : ℕ∞) ≤ N) (x : E) :
    iteratedFderiv 𝕜 k (fun y => ∑' n, f n y) x = ∑' n, iteratedFderiv 𝕜 k (f n) x := by
  rw [iteratedFderiv_tsum hf hv h'f hk]
#align iterated_fderiv_tsum_apply iteratedFderiv_tsum_apply

/-- Consider a series of functions `∑' i, f i x`. Assume that each individual function `f i` is of
class `C^N`, and moreover there is a uniform summable upper bound on the `k`-th derivative
for each `k ≤ N`. Then the series is also `C^N`. -/
theorem contDiff_tsum (hf : ∀ i, ContDiff 𝕜 N (f i)) (hv : ∀ k : ℕ, (k : ℕ∞) ≤ N → Summable (v k))
    (h'f : ∀ (k : ℕ) (i : α) (x : E), (k : ℕ∞) ≤ N → ‖iteratedFderiv 𝕜 k (f i) x‖ ≤ v k i) :
    ContDiff 𝕜 N fun x => ∑' i, f i x :=
  by
  rw [contDiff_iff_continuous_differentiable]
  constructor
  · intro m hm
    rw [iteratedFderiv_tsum hf hv h'f hm]
    refine' continuous_tsum _ (hv m hm) _
    · intro i
      exact ContDiff.continuous_iteratedFderiv hm (hf i)
    · intro n x
      exact h'f _ _ _ hm
  · intro m hm
    have h'm : ((m + 1 : ℕ) : ℕ∞) ≤ N := by
      simpa only [ENat.coe_add, Nat.cast_withBot, ENat.coe_one] using ENat.add_one_le_of_lt hm
    rw [iteratedFderiv_tsum hf hv h'f hm.le]
    have A :
      ∀ n x, HasFderivAt (iteratedFderiv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFderiv 𝕜 m (f n)) x) x :=
      fun n x => (ContDiff.differentiable_iteratedFderiv hm (hf n)).DifferentiableAt.HasFderivAt
    apply differentiable_tsum (hv _ h'm) A fun n x => _
    rw [fderiv_iteratedFderiv, LinearIsometryEquiv.norm_map]
    exact h'f _ _ _ h'm
#align cont_diff_tsum contDiff_tsum

/-- Consider a series of functions `∑' i, f i x`. Assume that each individual function `f i` is of
class `C^N`, and moreover there is a uniform summable upper bound on the `k`-th derivative
for each `k ≤ N` (except maybe for finitely many `i`s). Then the series is also `C^N`. -/
theorem contDiff_tsum_of_eventually (hf : ∀ i, ContDiff 𝕜 N (f i))
    (hv : ∀ k : ℕ, (k : ℕ∞) ≤ N → Summable (v k))
    (h'f :
      ∀ k : ℕ,
        (k : ℕ∞) ≤ N →
          ∀ᶠ i in (Filter.cofinite : Filter α), ∀ x : E, ‖iteratedFderiv 𝕜 k (f i) x‖ ≤ v k i) :
    ContDiff 𝕜 N fun x => ∑' i, f i x := by
  classical
    apply contDiff_iff_forall_nat_le.2 fun m hm => _
    let t : Set α :=
      { i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFderiv 𝕜 k (f i) x‖ ≤ v k i }
    have ht : Set.Finite t :=
      haveI A :
        ∀ᶠ i in (Filter.cofinite : Filter α),
          ∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFderiv 𝕜 k (f i) x‖ ≤ v k i :=
        by
        rw [eventually_all_finset]
        intro i hi
        apply h'f
        simp only [Finset.mem_range_succ_iff] at hi
        exact (WithTop.coe_le_coe.2 hi).trans hm
      eventually_cofinite.2 A
    let T : Finset α := ht.to_finset
    have :
      (fun x => ∑' i, f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' i : { i // i ∉ T }, f i x :=
      by
      ext1 x
      refine' (sum_add_tsum_subtype_compl _ T).symm
      refine' summable_of_norm_bounded_eventually _ (hv 0 (zero_le _)) _
      filter_upwards [h'f 0 (zero_le _)]with i hi
      simpa only [norm_iteratedFderiv_zero] using hi x
    rw [this]
    apply (ContDiff.sum fun i hi => (hf i).of_le hm).add
    have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ (coe : { i // i ∉ T } → α)) := fun k hk =>
      (hv k (hk.trans hm)).Subtype _
    refine' contDiff_tsum (fun i => (hf i).of_le hm) h'u _
    rintro k ⟨i, hi⟩ x hk
    dsimp
    simp only [finite.mem_to_finset, mem_set_of_eq, Finset.mem_range, not_forall, not_le,
      exists_prop, not_exists, not_and, not_lt] at hi
    exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x
#align cont_diff_tsum_of_eventually contDiff_tsum_of_eventually

author: leanprover-community


text:
import data.set.intervals
import analysis.mean_inequalities_pow

import for_mathlib.nnreal
import for_mathlib.Profinite.extend
import pseudo_normed_group.category
import condensed.ab

.

open_locale big_operators nnreal

universe u
variables (p : ℝ≥0) (S : Fintype.{u})

/-- The functor represented by ℤ, i.e., sending a finite type `S` to `S → ℤ`,
  equipped with the "p-norm" sending `s ↦ f(s)` to `∑ₛ∥f(s)∥₊ᵖ`. This is the
  construction defined as a bare function. -/
@[derive add_comm_group]
def normed_free_pfpng (p : ℝ≥0) (S : Fintype.{u}) := S → ℤ

noncomputable theory
open_locale classical

instance : has_nnnorm (normed_free_pfpng p S) :=
⟨λ f, ∑ s, ∥f s∥₊ ^ (p:ℝ)⟩

namespace normed_free_pfpng

protected lemma nnnorm_def (f : normed_free_pfpng p S) : ∥f∥₊ = ∑ s, ∥f s∥₊ ^ (p:ℝ) := rfl

@[simp] lemma nnnorm_zero [fact (0 < p)] : ∥(0 : normed_free_pfpng p S)∥₊ = 0 :=
by { change ∑ _, _ = _, simp only [pi.zero_apply, nnnorm_zero, finset.sum_const, nsmul_eq_mul, mul_eq_zero, nat.cast_eq_zero, finset.card_eq_zero,
  nnreal.rpow_eq_zero_iff, eq_self_iff_true, ne.def, nnreal.coe_eq_zero, true_and],
  right, have : 0 < p := fact.out _, exact this.ne' }

@[simp] lemma nnnorm_neg (f : normed_free_pfpng p S) : ∥(-f)∥₊ = ∥f∥₊ :=
by { change ∑ _, _ = _, simpa }

lemma nnnorm_add [fact (0 ≤ p)] [fact (p ≤ 1)]
  (f₁ f₂ : normed_free_pfpng p S) : ∥f₁ + f₂∥₊ ≤ ∥f₁∥₊ + ∥f₂∥₊ :=
begin
  change ∑ _, _ ≤ ∑ _, _ + ∑ _, _,
  rw ← finset.sum_add_distrib,
  apply finset.sum_le_sum,
  intros s _,
  have h0p : 0 ≤ p := fact.out _,
  have hp1 : p ≤ 1 := fact.out _,
  calc ∥(f₁ + f₂) s∥₊ ^ ↑p
      ≤ (∥f₁ s∥₊ + ∥f₂ s∥₊) ^ ↑p : nnreal.rpow_le_rpow (nnnorm_add_le _ _) h0p
  ... ≤ ∥f₁ s∥₊ ^ ↑p + ∥f₂ s∥₊ ^ ↑p : nnreal.rpow_add_le_add_rpow _ _ h0p hp1,
end

instance (c) : topological_space { f : normed_free_pfpng p S | ∥f∥₊ ≤ c } := ⊥
instance (c) : discrete_topology { f : normed_free_pfpng p S | ∥f∥₊ ≤ c } := ⟨rfl⟩

lemma norm_eval_le {c : nnreal} (s : S)
  (f : normed_free_pfpng p S) (hf : ∥f∥₊ ≤ c) : ∥f s∥₊ ^ (p:ℝ) ≤ c :=
le_trans (begin
  apply @finset.single_le_sum S nnreal _ (λ t, ∥f t∥₊ ^ (p:ℝ)) finset.univ,
  { intros _ _, apply zero_le },
  { exact finset.mem_univ s }
end) hf

instance [fact (0 < p)] (c) : fintype { f : normed_free_pfpng p S | ∥f∥₊ ≤ c } :=
begin
  let A := { f : normed_free_pfpng p S | ∥f∥₊ ≤ c },
  let N := ⌈c ^ (p⁻¹:ℝ)⌉₊,
  have hN := @nat.le_ceil ℝ≥0 _ _ (c ^ (p⁻¹:ℝ)),
  have h0p : 0 < p := fact.out _,
  have h0pinv : 0 ≤ p⁻¹, { rw ← nnreal.inv_pos at h0p, exact h0p.le },
  let ι : A → S → set.Icc (-(N : ℤ)) N :=
    λ a s, ⟨a.1 s, _⟩,
  swap,
  { have := (nnreal.rpow_le_rpow (norm_eval_le p S s a.val a.2) h0pinv).trans hN,
    rw [← nnreal.coe_le_coe, ← nnreal.rpow_mul, ← nnreal.coe_mul,
      mul_inv_cancel h0p.ne', nnreal.coe_one, nnreal.rpow_one, nnreal.coe_nat_cast] at this,
    split,
    { rw [← neg_le_neg_iff] at this,
      exact_mod_cast this.trans (neg_abs_le_self (a.val s)), },
    { exact_mod_cast (le_abs_self _).trans this, } },
  have : function.injective ι,
  { rintros ⟨f,hf⟩ ⟨g,hg⟩ h,
    ext s,
    apply_fun (λ e, (e s).1) at h,
    assumption },
  apply fintype.of_injective ι this,
end

variables [fact (0 < p)] [fact (p ≤ 1)]

instance : profinitely_filtered_pseudo_normed_group (normed_free_pfpng p S) :=
{ filtration := λ c, { f | ∥ f ∥₊ ≤ c },
  filtration_mono := λ c₁ c₂ h f hf, le_trans hf h,
  zero_mem_filtration := λ c, by simp,
  neg_mem_filtration := λ c f hf, by simpa,
  add_mem_filtration := λ c₁ c₂ f₁ f₂ h₁ h₂,
    le_trans (nnnorm_add _ _ _ _) (add_le_add h₁ h₂),
  continuous_add' := λ c₁ c₂,
    continuous_of_discrete_topology,
  continuous_neg' := λ c, continuous_of_discrete_topology,
  continuous_cast_le := λ _ _ _, continuous_of_discrete_topology,
  ..(infer_instance : add_comm_group (normed_free_pfpng p S)) }

def map {S₁ S₂ : Fintype.{u}} (g : S₁ ⟶ S₂) :
  strict_comphaus_filtered_pseudo_normed_group_hom
  (normed_free_pfpng p S₁) (normed_free_pfpng p S₂) :=
{ to_fun := λ f s, ∑ t in finset.univ.filter (λ w, g w = s), f t,
  map_zero' := by simpa,
  map_add' := λ f g, by simpa [finset.sum_add_distrib],
  strict' := begin
    have h0p : 0 < p := fact.out _,
    have hp1 : p ≤ 1 := fact.out _,
    intros c f hf,
    refine le_trans _ hf,
    simp only [normed_free_pfpng.nnnorm_def],
    have : ∑ s₂, ∥(∑ t in finset.univ.filter (λ w, g w = s₂), f t)∥₊ ^ (p:ℝ) ≤
      ∑ s₂ : S₂, ∑ t in finset.univ.filter (λ w, g w = s₂), ∥f t∥₊ ^ (p:ℝ),
    { apply finset.sum_le_sum,
      intros i _,
      refine le_trans _ (nnreal.rpow_sum_le_sum_rpow _ _ h0p hp1),
      refine nnreal.rpow_le_rpow _ h0p.le,
      apply nnnorm_sum_le },
    refine le_trans this _,
    rw ← finset.sum_bUnion,
    apply le_of_eq,
    apply finset.sum_congr,
    { rw finset.eq_univ_iff_forall,
      intros x,
      rw finset.mem_bUnion,
      use [g x, by simp] },
    { intros s₁ _, refl },
    { intros x _ y _ h,
      rintros a hh,
      apply h,
      simp only [finset.inf_eq_inter, finset.mem_inter, finset.mem_filter,
        finset.mem_univ, true_and] at hh,
      rw [← hh.1, ← hh.2] }
  end,
  continuous' := λ c, continuous_of_discrete_topology }

@[simp]
lemma map_id : map p (𝟙 S) =
  strict_comphaus_filtered_pseudo_normed_group_hom.id :=
begin
  ext s,
  dsimp [map],
  simp [finset.filter_congr_decidable, finset.sum_filter],
end

@[simp]
lemma map_comp {S₁ S₂ S₃ : Fintype.{u}}
  (g₁ : S₁ ⟶ S₂) (g₂ : S₂ ⟶ S₃) :
  map p (g₁ ≫ g₂) =
  (map p g₂).comp (map p g₁) :=
begin
  ext s₃,
  dsimp [map],
  erw ← finset.sum_bUnion,
  apply finset.sum_congr,
  { ext s,
    split,
    { intro h, simp only [finset.mem_filter, finset.mem_univ, true_and] at h,
      rw finset.mem_bUnion,
      use [g₁ s, by simpa] },
    { intro h, simp only [finset.mem_bUnion, finset.mem_filter,
      finset.mem_univ, true_and, exists_prop, exists_eq_right'] at h,
      simpa, } },
  { intros s₁ h,
    rw finset.mem_bUnion at h },
  { intros x hx y hy,
    simp only [finset.coe_filter, finset.coe_univ, set.sep_univ,
      set.mem_set_of_eq] at hx hy,
    intros h a ha,
    simp only [finset.inf_eq_inter, finset.mem_inter, finset.mem_filter,
      finset.mem_univ, true_and] at ha,
    apply h, rw [← ha.1, ← ha.2] }
end

end normed_free_pfpng

variables [fact (0 < p)] [fact (p ≤ 1)]

/-- The functor represented by ℤ, i.e., sending a finite type `S` to
  `normed_free_pfpng p S`, otherwise known as `S → ℤ`,
  equipped with the "p-norm" sending `s ↦ f(s)` to `∑ₛ∥f(s)∥₊ᵖ`. This norm
  makes `S → ℤ` into a `profinitely_filtered_pseudo_normed_group`. -/
@[simps]
def normed_free_pfpng_functor : Fintype ⥤ ProFiltPseuNormGrp₁ :=
{ obj := λ S,
  { M := normed_free_pfpng p S,
    exhaustive' := λ f, ⟨∥f∥₊, le_refl _⟩ },
  map := λ S₁ S₂ f, normed_free_pfpng.map p f,
  map_id' := λ S, normed_free_pfpng.map_id p S,
  map_comp' := λ _ _ _ g₁ g₂, normed_free_pfpng.map_comp p g₁ g₂ }

def Fintype.normed_free_pfpng (T : Fintype) : ProFiltPseuNormGrp₁ :=
(normed_free_pfpng_functor p).obj T

def Fintype.normed_free_pfpng_unit :
  Fintype.to_Profinite ⟶ normed_free_pfpng_functor p ⋙ ProFiltPseuNormGrp₁.level.obj 1 :=
{ app := λ S,
  { to_fun := λ s,
    { val := λ t, if s = t then 1 else 0,
      property := begin
        show finset.sum _ _ ≤ _,
        rw finset.sum_eq_single_of_mem,
        swap 4, { exact s }, swap 2, { apply finset.mem_univ },
        { dsimp, rw [if_pos rfl, nnnorm_one, nnreal.one_rpow], },
        rintro t - ht, dsimp, rw [if_neg ht.symm, nnnorm_zero, nnreal.zero_rpow],
        have h0p : 0 < p := fact.out _, exact_mod_cast h0p.ne',
      end },
    continuous_to_fun := continuous_bot },
  naturality' := λ S T f, begin
    ext s t,
    delta ProFiltPseuNormGrp₁.level,
    simp only [Fintype.to_Profinite_map_apply, Profinite.coe_comp, continuous_map.coe_mk,
      function.comp_app, subtype.coe_mk, category_theory.functor.comp_map, normed_free_pfpng_functor_map,
      pseudo_normed_group.level_coe, subtype.coe_mk, normed_free_pfpng.map, finset.mem_filter, true_and,
      finset.mem_univ, strict_comphaus_filtered_pseudo_normed_group_hom.coe_mk, finset.sum_ite_eq],
  end }

def Profinite.normed_free_pfpng (S : Profinite) : ProFiltPseuNormGrp₁ :=
(Profinite.extend $ normed_free_pfpng_functor p).obj S

open category_theory
open category_theory.limits

def Profinite.normed_free_pfpng_level_iso (S : Profinite.{u}) (r) :
  (ProFiltPseuNormGrp₁.level.obj r).obj (S.normed_free_pfpng p) ≅
  limits.limit (S.fintype_diagram ⋙ normed_free_pfpng_functor p ⋙ ProFiltPseuNormGrp₁.level.obj r) :=
(is_limit_of_preserves (ProFiltPseuNormGrp₁.level.obj r)
  (limit.is_limit _)).cone_point_unique_up_to_iso $ limit.is_limit _

def Profinite.to_normed_free_pfpng (S : Profinite.{u}) :
  S ⟶ (ProFiltPseuNormGrp₁.level.obj 1).obj (S.normed_free_pfpng p) :=
(limit.is_limit _).map S.as_limit_cone (whisker_left _ $ Fintype.normed_free_pfpng_unit.{u u} p) ≫
(S.normed_free_pfpng_level_iso p 1).inv

--(limits.is_limit_of_preserves (ProFiltPseuNormGrp₁.level.obj 1) (limits.limit.is_limit _)).map
--  S.as_limit_cone $ whisker_left _ (Fintype.normed_free_pfpng_unit) ≫ (functor.associator _ _ _).inv

def Profinite.normed_free_pfpng_π (S : Profinite) (T : discrete_quotient S) :
  S.normed_free_pfpng p ⟶ (Fintype.of T).normed_free_pfpng p :=
category_theory.limits.limit.π _ _

lemma Profinite.normed_free_pfpng_π_w (S : Profinite) {T₁ T₂ : discrete_quotient S} (f : T₁ ⟶ T₂) :
  Profinite.normed_free_pfpng_π p S T₁ ≫ (S.fintype_diagram ⋙ normed_free_pfpng_functor p).map f =
  Profinite.normed_free_pfpng_π p S T₂ :=
category_theory.limits.limit.w (S.fintype_diagram ⋙ normed_free_pfpng_functor p) _

repo: lean-liquid


text:
/-
Copyright (c) 2020 Joseph Myers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Myers, Sébastien Gouëzel, Heather Macbeth
-/
import analysis.inner_product_space.projection
import analysis.normed_space.pi_Lp

/-!
# `L²` inner product space structure on finite products of inner product spaces

The `L²` norm on a finite product of inner product spaces is compatible with an inner product
$$
\langle x, y\rangle = \sum \langle x_i, y_i \rangle.
$$
This is recorded in this file as an inner product space instance on `pi_Lp 2`.

## Main definitions

- `euclidean_space 𝕜 n`: defined to be `pi_Lp 2 (n → 𝕜)` for any `fintype n`, i.e., the space
  from functions to `n` to `𝕜` with the `L²` norm. We register several instances on it (notably
  that it is a finite-dimensional inner product space).

- `basis.isometry_euclidean_of_orthonormal`: provides the isometry to Euclidean space
  from a given finite-dimensional inner product space, induced by a basis of the space.

- `linear_isometry_equiv.of_inner_product_space`: provides an arbitrary isometry to Euclidean space
  from a given finite-dimensional inner product space, induced by choosing an arbitrary basis.

- `complex.isometry_euclidean`: standard isometry from `ℂ` to `euclidean_space ℝ (fin 2)`

-/

open real set filter is_R_or_C
open_locale big_operators uniformity topological_space nnreal ennreal complex_conjugate direct_sum

noncomputable theory

variables {ι : Type*}
variables {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [inner_product_space 𝕜 E]
local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

/-
 If `ι` is a finite type and each space `f i`, `i : ι`, is an inner product space,
then `Π i, f i` is an inner product space as well. Since `Π i, f i` is endowed with the sup norm,
we use instead `pi_Lp 2 f` for the product space, which is endowed with the `L^2` norm.
-/
instance pi_Lp.inner_product_space {ι : Type*} [fintype ι] (f : ι → Type*)
  [Π i, inner_product_space 𝕜 (f i)] : inner_product_space 𝕜 (pi_Lp 2 f) :=
{ inner := λ x y, ∑ i, inner (x i) (y i),
  norm_sq_eq_inner :=
  begin
    intro x,
    have h₁ : ∑ (i : ι), ∥x i∥ ^ (2 : ℕ) = ∑ (i : ι), ∥x i∥ ^ (2 : ℝ),
    { apply finset.sum_congr rfl,
      intros j hj,
      simp [←rpow_nat_cast] },
    have h₂ : 0 ≤ ∑ (i : ι), ∥x i∥ ^ (2 : ℝ),
    { rw [←h₁],
      exact finset.sum_nonneg (λ j (hj : j ∈ finset.univ), pow_nonneg (norm_nonneg (x j)) 2) },
    simp [norm, add_monoid_hom.map_sum, ←norm_sq_eq_inner],
    rw [←rpow_nat_cast ((∑ (i : ι), ∥x i∥ ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹) 2],
    rw [←rpow_mul h₂],
    norm_num [h₁],
  end,
  conj_sym :=
  begin
    intros x y,
    unfold inner,
    rw ring_hom.map_sum,
    apply finset.sum_congr rfl,
    rintros z -,
    apply inner_conj_sym,
  end,
  add_left := λ x y z,
    show ∑ i, inner (x i + y i) (z i) = ∑ i, inner (x i) (z i) + ∑ i, inner (y i) (z i),
    by simp only [inner_add_left, finset.sum_add_distrib],
  smul_left := λ x y r,
    show ∑ (i : ι), inner (r • x i) (y i) = (conj r) * ∑ i, inner (x i) (y i),
    by simp only [finset.mul_sum, inner_smul_left] }

@[simp] lemma pi_Lp.inner_apply {ι : Type*} [fintype ι] {f : ι → Type*}
  [Π i, inner_product_space 𝕜 (f i)] (x y : pi_Lp 2 f) :
  ⟪x, y⟫ = ∑ i, ⟪x i, y i⟫ :=
rfl

lemma pi_Lp.norm_eq_of_L2 {ι : Type*} [fintype ι] {f : ι → Type*}
  [Π i, inner_product_space 𝕜 (f i)] (x : pi_Lp 2 f) :
  ∥x∥ = sqrt (∑ (i : ι), ∥x i∥ ^ 2) :=
by { rw [pi_Lp.norm_eq_of_nat 2]; simp [sqrt_eq_rpow] }

/-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `euclidean_space 𝕜 (fin n)`. -/
@[reducible, nolint unused_arguments]
def euclidean_space (𝕜 : Type*) [is_R_or_C 𝕜]
  (n : Type*) [fintype n] : Type* := pi_Lp 2 (λ (i : n), 𝕜)

lemma euclidean_space.norm_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
  (x : euclidean_space 𝕜 n) : ∥x∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2) :=
pi_Lp.norm_eq_of_L2 x

section
local attribute [reducible] pi_Lp

variables [fintype ι]

instance : finite_dimensional 𝕜 (euclidean_space 𝕜 ι) := by apply_instance
instance : inner_product_space 𝕜 (euclidean_space 𝕜 ι) := by apply_instance

@[simp] lemma finrank_euclidean_space :
  finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 ι) = fintype.card ι := by simp

lemma finrank_euclidean_space_fin {n : ℕ} :
  finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 (fin n)) = n := by simp

/-- A finite, mutually orthogonal family of subspaces of `E`, which span `E`, induce an isometry
from `E` to `pi_Lp 2` of the subspaces equipped with the `L2` inner product. -/
def direct_sum.submodule_is_internal.isometry_L2_of_orthogonal_family
  [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.submodule_is_internal V)
  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
  E ≃ₗᵢ[𝕜] pi_Lp 2 (λ i, V i) :=
begin
  let e₁ := direct_sum.linear_equiv_fun_on_fintype 𝕜 ι (λ i, V i),
  let e₂ := linear_equiv.of_bijective _ hV.injective hV.surjective,
  refine (e₂.symm.trans e₁).isometry_of_inner _,
  suffices : ∀ v w, ⟪v, w⟫ = ⟪e₂ (e₁.symm v), e₂ (e₁.symm w)⟫,
  { intros v₀ w₀,
    convert this (e₁ (e₂.symm v₀)) (e₁ (e₂.symm w₀));
    simp only [linear_equiv.symm_apply_apply, linear_equiv.apply_symm_apply] },
  intros v w,
  transitivity ⟪(∑ i, (V i).subtypeₗᵢ (v i)), ∑ i, (V i).subtypeₗᵢ (w i)⟫,
  { simp only [sum_inner, hV'.inner_right_fintype, pi_Lp.inner_apply] },
  { congr; simp }
end

@[simp] lemma direct_sum.submodule_is_internal.isometry_L2_of_orthogonal_family_symm_apply
  [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.submodule_is_internal V)
  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ))
  (w : pi_Lp 2 (λ i, V i)) :
  (hV.isometry_L2_of_orthogonal_family hV').symm w = ∑ i, (w i : E) :=
begin
  classical,
  let e₁ := direct_sum.linear_equiv_fun_on_fintype 𝕜 ι (λ i, V i),
  let e₂ := linear_equiv.of_bijective _ hV.injective hV.surjective,
  suffices : ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i,
  { exact this (e₁.symm w) },
  intros v,
  simp [e₂, direct_sum.submodule_coe, direct_sum.to_module, dfinsupp.sum_add_hom_apply]
end

/-- An orthonormal basis on a fintype `ι` for an inner product space induces an isometry with
`euclidean_space 𝕜 ι`. -/
def basis.isometry_euclidean_of_orthonormal
  (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) :
  E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι :=
v.equiv_fun.isometry_of_inner
begin
  intros x y,
  let p : euclidean_space 𝕜 ι := v.equiv_fun x,
  let q : euclidean_space 𝕜 ι := v.equiv_fun y,
  have key : ⟪p, q⟫ = ⟪∑ i, p i • v i, ∑ i, q i • v i⟫,
  { simp [sum_inner, inner_smul_left, hv.inner_right_fintype] },
  convert key,
  { rw [← v.equiv_fun.symm_apply_apply x, v.equiv_fun_symm_apply] },
  { rw [← v.equiv_fun.symm_apply_apply y, v.equiv_fun_symm_apply] }
end

@[simp] lemma basis.coe_isometry_euclidean_of_orthonormal
  (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) :
  (v.isometry_euclidean_of_orthonormal hv : E → euclidean_space 𝕜 ι) = v.equiv_fun :=
rfl

@[simp] lemma basis.coe_isometry_euclidean_of_orthonormal_symm
  (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) :
  ((v.isometry_euclidean_of_orthonormal hv).symm : euclidean_space 𝕜 ι → E) = v.equiv_fun.symm :=
rfl

end

/-- `ℂ` is isometric to `ℝ²` with the Euclidean inner product. -/
def complex.isometry_euclidean : ℂ ≃ₗᵢ[ℝ] (euclidean_space ℝ (fin 2)) :=
complex.basis_one_I.isometry_euclidean_of_orthonormal
begin
  rw orthonormal_iff_ite,
  intros i, fin_cases i;
  intros j; fin_cases j;
  simp [real_inner_eq_re_inner]
end

@[simp] lemma complex.isometry_euclidean_symm_apply (x : euclidean_space ℝ (fin 2)) :
  complex.isometry_euclidean.symm x = (x 0) + (x 1) * I :=
begin
  convert complex.basis_one_I.equiv_fun_symm_apply x,
  { simpa },
  { simp },
end

lemma complex.isometry_euclidean_proj_eq_self (z : ℂ) :
  ↑(complex.isometry_euclidean z 0) + ↑(complex.isometry_euclidean z 1) * (I : ℂ) = z :=
by rw [← complex.isometry_euclidean_symm_apply (complex.isometry_euclidean z),
  complex.isometry_euclidean.symm_apply_apply z]

@[simp] lemma complex.isometry_euclidean_apply_zero (z : ℂ) :
  complex.isometry_euclidean z 0 = z.re :=
by { conv_rhs { rw ← complex.isometry_euclidean_proj_eq_self z }, simp }

@[simp] lemma complex.isometry_euclidean_apply_one (z : ℂ) :
  complex.isometry_euclidean z 1 = z.im :=
by { conv_rhs { rw ← complex.isometry_euclidean_proj_eq_self z }, simp }

open finite_dimensional

/-- Given a natural number `n` equal to the `finrank` of a finite-dimensional inner product space,
there exists an isometry from the space to `euclidean_space 𝕜 (fin n)`. -/
def linear_isometry_equiv.of_inner_product_space
  [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
  E ≃ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n)) :=
(fin_orthonormal_basis hn).isometry_euclidean_of_orthonormal (fin_orthonormal_basis_orthonormal hn)

local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ

/-- Given a natural number `n` one less than the `finrank` of a finite-dimensional inner product
space, there exists an isometry from the orthogonal complement of a nonzero singleton to
`euclidean_space 𝕜 (fin n)`. -/
def linear_isometry_equiv.from_orthogonal_span_singleton
  (n : ℕ) [fact (finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
  (𝕜 ∙ v)ᗮ ≃ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n)) :=
linear_isometry_equiv.of_inner_product_space (finrank_orthogonal_span_singleton hv)

author: Mel-TunaRoll

repo: Lean-Mordell-Weil-Mel-Branch


text:
/-
Copyright (c) 2020 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.data.polynomial.ring_division
import Mathlib.data.mv_polynomial.rename
import Mathlib.ring_theory.polynomial.basic
import Mathlib.PostPort

universes u_1 u_2

namespace Mathlib

/-!
## Function extensionality for multivariate polynomials

In this file we show that two multivariate polynomials over an infinite integral domain are equal
if they are equal upon evaluating them on an arbitrary assignment of the variables.

# Main declaration

* `mv_polynomial.funext`: two polynomials `φ ψ : mv_polynomial σ R`
  over an infinite integral domain `R` are equal if `eval x φ = eval x ψ` for all `x : σ → R`.

-/

namespace mv_polynomial

/-- Two multivariate polynomials over an infinite integral domain are equal
if they are equal upon evaluating them on an arbitrary assignment of the variables. -/
theorem funext {R : Type u_1} [integral_domain R] [infinite R] {σ : Type u_2} {p : mv_polynomial σ R} {q : mv_polynomial σ R} (h : ∀ (x : σ → R), coe_fn (eval x) p = coe_fn (eval x) q) : p = q := sorry

theorem funext_iff {R : Type u_1} [integral_domain R] [infinite R] {σ : Type u_2} {p : mv_polynomial σ R} {q : mv_polynomial σ R} : p = q ↔ ∀ (x : σ → R), coe_fn (eval x) p = coe_fn (eval x) q := sorry

author: AurelienSaue


text:
/-
Copyright (c) 2019 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import category_theory.endomorphism

/-!
# Conjugate morphisms by isomorphisms

An isomorphism `α : X ≅ Y` defines
- a monoid isomorphism `conj : End X ≃* End Y` by `α.conj f = α.inv ≫ f ≫ α.hom`;
- a group isomorphism `conj_Aut : Aut X ≃* Aut Y` by `α.conj_Aut f = α.symm ≪≫ f ≪≫ α`.

For completeness, we also define `hom_congr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁)`,
cf. `equiv.arrow_congr`.
-/

universes v u

namespace category_theory

namespace iso

variables {C : Type u} [category.{v} C]

/-- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
there is a natural bijection between `X ⟶ Y` and `X₁ ⟶ Y₁`. See also `equiv.arrow_congr`. -/
def hom_congr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) :
  (X ⟶ Y) ≃ (X₁ ⟶ Y₁) :=
{ to_fun := λ f, α.inv ≫ f ≫ β.hom,
  inv_fun := λ f, α.hom ≫ f ≫ β.inv,
  left_inv := λ f, show α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f,
    by rw [category.assoc, category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, category.comp_id],
  right_inv := λ f, show α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f,
    by rw [category.assoc, category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, category.comp_id] }

@[simp]
lemma hom_congr_apply {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :
  α.hom_congr β f = α.inv ≫ f ≫ β.hom :=
rfl

lemma hom_congr_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁)
  (f : X ⟶ Y) (g : Y ⟶ Z) :
  α.hom_congr γ (f ≫ g) = α.hom_congr β f ≫ β.hom_congr γ g :=
by simp

@[simp] lemma hom_congr_refl {X Y : C} (f : X ⟶ Y) :
  (iso.refl X).hom_congr (iso.refl Y) f = f :=
by simp

@[simp] lemma hom_congr_trans {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C}
  (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) (f : X₁ ⟶ Y₁) :
  (α₁ ≪≫ α₂).hom_congr (β₁ ≪≫ β₂) f = (α₁.hom_congr β₁).trans (α₂.hom_congr β₂) f :=
by simp

@[simp] lemma hom_congr_symm {X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) :
  (α.hom_congr β).symm = α.symm.hom_congr β.symm :=
rfl

variables {X Y : C} (α : X ≅ Y)

/-- An isomorphism between two objects defines a monoid isomorphism between their
monoid of endomorphisms. -/
def conj : End X ≃* End Y :=
{ map_mul' := λ f g, hom_congr_comp α α α g f,
  .. hom_congr α α }

lemma conj_apply (f : End X) : α.conj f = α.inv ≫ f ≫ α.hom := rfl

@[simp] lemma conj_comp (f g : End X) : α.conj (f ≫ g) = (α.conj f) ≫ (α.conj g) :=
α.conj.map_mul g f

@[simp] lemma conj_id : α.conj (𝟙 X) = 𝟙 Y :=
α.conj.map_one

@[simp] lemma refl_conj (f : End X) : (iso.refl X).conj f = f :=
by rw [conj_apply, iso.refl_inv, iso.refl_hom, category.id_comp, category.comp_id]

@[simp] lemma trans_conj {Z : C} (β : Y ≅ Z) (f : End X) : (α ≪≫ β).conj f = β.conj (α.conj f) :=
hom_congr_trans α α β β f

@[simp] lemma symm_self_conj (f : End X) : α.symm.conj (α.conj f) = f :=
by rw [← trans_conj, α.self_symm_id, refl_conj]

@[simp] lemma self_symm_conj (f : End Y) : α.conj (α.symm.conj f) = f :=
α.symm.symm_self_conj f

@[simp] lemma conj_pow (f : End X) (n : ℕ) : α.conj (f^n) = (α.conj f)^n :=
α.conj.to_monoid_hom.map_pow f n

/-- `conj` defines a group isomorphisms between groups of automorphisms -/
def conj_Aut : Aut X ≃* Aut Y :=
(Aut.units_End_equiv_Aut X).symm.trans $
(units.map_equiv α.conj).trans $
Aut.units_End_equiv_Aut Y

lemma conj_Aut_apply (f : Aut X) : α.conj_Aut f = α.symm ≪≫ f ≪≫ α :=
by cases f; cases α; ext; refl

@[simp] lemma conj_Aut_hom (f : Aut X) : (α.conj_Aut f).hom = α.conj f.hom := rfl

@[simp] lemma trans_conj_Aut {Z : C} (β : Y ≅ Z) (f : Aut X) :
  (α ≪≫ β).conj_Aut f = β.conj_Aut (α.conj_Aut f) :=
by simp only [conj_Aut_apply, iso.trans_symm, iso.trans_assoc]

@[simp] lemma conj_Aut_mul (f g : Aut X) : α.conj_Aut (f * g) = α.conj_Aut f * α.conj_Aut g :=
α.conj_Aut.map_mul f g

@[simp] lemma conj_Aut_trans (f g : Aut X) : α.conj_Aut (f ≪≫ g) = α.conj_Aut f ≪≫ α.conj_Aut g :=
conj_Aut_mul α g f

@[simp] lemma conj_Aut_pow (f : Aut X) (n : ℕ) : α.conj_Aut (f^n) = (α.conj_Aut f)^n :=
α.conj_Aut.to_monoid_hom.map_pow f n

@[simp] lemma conj_Aut_zpow (f : Aut X) (n : ℤ) : α.conj_Aut (f^n) = (α.conj_Aut f)^n :=
α.conj_Aut.to_monoid_hom.map_zpow f n

end iso

namespace functor

universes v₁ u₁

variables {C : Type u} [category.{v} C] {D : Type u₁} [category.{v₁} D] (F : C ⥤ D)

lemma map_hom_congr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :
  F.map (iso.hom_congr α β f) = iso.hom_congr (F.map_iso α) (F.map_iso β) (F.map f) :=
by simp

lemma map_conj {X Y : C} (α : X ≅ Y) (f : End X) :
  F.map (α.conj f) = (F.map_iso α).conj (F.map f) :=
map_hom_congr F α α f

lemma map_conj_Aut (F : C ⥤ D) {X Y : C} (α : X ≅ Y) (f : Aut X) :
  F.map_iso (α.conj_Aut f) = (F.map_iso α).conj_Aut (F.map_iso f) :=
by ext; simp only [map_iso_hom, iso.conj_Aut_hom, F.map_conj]
-- alternative proof: by simp only [iso.conj_Aut_apply, F.map_iso_trans, F.map_iso_symm]

end functor
end category_theory

author: jjaassoonn


import combinatorics.simple_graph.coloring

--OUTPUT 1
theorem bipartite_iff_two_colorable (G : Type*) [graph G] : bipartite G ↔ two_colorable G :=
begin
  split,
  { assume h,
    suffices h1 : ∃ A B : set G, A ∩ B = ∅ ∧ A ∪ B = G.V ∧ ∀ x y ∈ G.E, x ∈ A → y ∈ B ∨ x ∈ B ∧ y ∈ A, from
    begin
      cases h1 with A h1,
      cases h1 with B h1,
      cases h1 with h1 h2,
      cases h2 with h2 h3,
      show two_colorable G, from by auto [two_colorable, two_coloring_def, h1, h2, h3],
    end,
    exact h,
  },
  { assume h,
    cases h with c h,
    cases h with c1 h,
    cases h with c2 h,
    cases h with h1 h2,
    cases h1 with h1 h3,
    cases h3 with h3 h4,
    have h5 : ∀ a b ∈ G.E, a ∈ c1.V → b ∈ c2.V ∨ a ∈ c2.V ∧ b ∈ c1.V, from by auto [h2],
    show bipartite G, from by auto [bipartite, h1, h3, h4, h5],
  },
end

--OUTPUT 2
theorem graph_bipartite_iff_two_colorable (G : Type*) [graph G] : two_colorable G ↔ bipartite G :=
begin
  split,
  {
    assume h,
    show bipartite G, from by auto [h, two_colorable_def]
  },
  {
    assume h,
    have h1 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h2 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h3 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h4 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h5 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h6 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h7 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h8 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h9 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h10 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h11 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h12 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h13 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h14 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h15 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h16 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h17 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h18 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h19 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h20 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h21 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h22 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h23 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h24 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h25 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h26 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h27 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h28 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h29 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h30 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h31 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h32 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h33 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) → (a ∈ (vertices G) ∧ a ∈ (vertices G)), from by auto,
    have h34 : ∀ a b : G, (a ∈ (vertices G) ∧ b ∈ (vertices G)) → (a ∈ (vertices G) ∧ b ∈ (vertices G)), from by auto,
    have h35 : ∀ a : G, (a ∈ (vertices G) ∧ a ∈ (vertices G)) →
end --Needs more than 2000 tokens!

--OUTPUT 3
theorem graph_bipartite_iff_two_colorable {α : Type*} (G : set (α × α)) :
    bipartite G ↔ two_colorable G :=
begin
  split,
  { assume h1 : bipartite G,
    obtain ⟨V1, V2, h2, h3⟩ := h1,
    use [V1, V2],
    assume [x y],
    assume h4 : (x, y) ∈ G,
    have h5 : (x ∈ V1) ∨ (x ∈ V2), from by auto [h2],
    have h6 : (y ∈ V1) ∨ (y ∈ V2), from by auto [h2],
    have h7 : (x ∈ V1) ∧ (y ∈ V2) ∨ (x ∈ V2) ∧ (y ∈ V1), from by auto [h5, h6],
    cases h7,
    { assume h8 : (x ∈ V1) ∧ (y ∈ V2),
      have h9 : (x, y) ∈ G, from by auto [h4],
      have h10 : (x, y) ∉ G, from by auto [h3, h8],
      contradiction },
    { assume h8 : (x ∈ V2) ∧ (y ∈ V1),
      have h9 : (x, y) ∈ G, from by auto [h4],
      have h10 : (x, y) ∉ G, from by auto [h3, h8],
      contradiction },
  },
  { assume h1 : two_colorable G,
    obtain ⟨V1, V2, h2, h3⟩ := h1,
    use [V1, V2],
    assume x y,
    assume h4 : (x, y) ∈ G,
    have h5 : (x ∈ V1) ∨ (x ∈ V2), from by auto [h2],
    have h6 : (y ∈ V1) ∨ (y ∈ V2), from by auto [h2],
    have h7 : (x ∈ V1) ∧ (y ∈ V1) ∨ (x ∈ V2) ∧ (y ∈ V2), from by auto [h5, h6],
    have h8 : (x ∈ V1) ∧ (y ∈ V1) → (x, y) ∉ G, from by auto [h3],
    have h9 : (x ∈ V2) ∧ (y ∈ V2) → (x, y) ∉ G, from by auto [h3],
    have h10 : (x ∈ V1) ∧ (y ∈ V1) ∨ (x ∈ V2) ∧ (y ∈ V2) → (x, y) ∉ G, from by auto [h8, h9],
    contradiction,
  }
end

--OUTPUT 4
theorem bipartite_graph_2_colorable (G : Type*) : ∃! A B : set G, is_bipartite G A B :=
begin
  have h1 : ∀ A B : set G, is_bipartite G A B → ∃! A B : set G, is_bipartite G A B, from by auto [exists_unique.unique, exists_unique.exists],
  have h2 : ∀ A B : set G, is_bipartite G A B → ∃! A B : set G, is_bipartite G A B, from by auto [exists_unique.unique, exists_unique.exists],
  show ∃! A B : set G, is_bipartite G A B, from by auto [h1, h2],
end

--OUTPUT 5
theorem bipartite_two_colorable {G : Type*} [graph G] : two_colorable G ↔ bipartite G :=
begin
  split,
  {intro h1,
  have h2 : ∃ V1 V2 : set G, (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1), from two_coloring.rec_on h1 (λ (V1 V2 : set G) h, exists.intro V1 (exists.intro V2 (and.intro (λ (v1 v2 : G), and.intro (λ (h1 : v1 ∈ V1 ∧ v2 ∈ V2), and.intro (λ (h2 : (v1, v2) ∈ edges G), false.elim (h v1 v2 h1 h2)) (λ (h2 : (v1, v2) ∈ edges G), false.elim (h v2 v1 (and.intro (and.elim_right h1) (and.elim_left h1)) (edge_comm h2)))))) (λ (v1 v2 : G), or.inr (and.intro (and.elim_left (h v1 v2)) (and.elim_right (h v1 v2))))))),
  have h3 : ∃ V1 V2 : set G, (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V2) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2), from (λ (V1 V2 : set G) (h : (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1)), exists.intro V1 (exists.intro V2 (and.intro h (λ (v : G), or.inr (and.intro (λ (h1), false.elim (h.left v v h1)) true.intro)))) h2),
  have h4 : ∃ V1 V2 : set G, (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2) ∧ (∀ (v : G), ¬ (v ∈ V1 ∧ v ∈ V2)), from exists.elim h3 (λ (V1 V2 : set G) (h : (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2)), exists.intro V1 (exists.intro V2 (and.intro (and.elim_left h) (and.intro (and.elim_left (and.elim_right h)) (and.intro (and.elim_right (and.elim_right h)) (λ (v : G), not_and.mp (not_or_distrib.mp (λ (h1 : ¬ (v ∈ V1 ∨ v ∈ V2)), h1.elim (λ (h2 : v ∈ V1), absurd (and.intro h2 h2) (h.left v v h2 h2)) (λ (h2 : v ∈ V2), absurd (and.intro h2 h2) (h.left v v h2 h2))))))))),
  have h5 : ∃ V1 V2 : set G, (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2) ∧ (∀ (v : G), ¬ (v ∈ V1 ∧ v ∈ V2)) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2 ∨ v ∉ G), from exists.elim h4 (λ (V1 V2 : set G) (h : (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2) ∧ (∀ (v : G), ¬ (v ∈ V1 ∧ v ∈ V2))), exists.intro V1 (exists.intro V2 (and.intro h (λ (v : G), or.inr (or.inr (or.elim (and.elim_left (and.elim_right h)) (λ (h1 : v ∈ V1), or.inl h1) (λ (h1 : v ∈ V2), or.inr h1) (λ (h1 : ¬ (v ∈ V1 ∨ v ∈ V2)), absurd h1 (and.elim_right (and.elim_right h))))))))),
  have h6 : ∃ V1 V2 : set G, (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2) ∧ (∀ (v : G), ¬ (v ∈ V1 ∧ v ∈ V2)) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2 ∨ v ∉ G) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2 ∨ v ∉ G), from exists.elim h5 (λ (V1 V2 : set G) (h : (∀ (v1 v2 : G), v1 ∈ V1 ∧ v2 ∈ V2 → ((v1, v2) ∈ edges G) → false) ∧ (∀ (v1 v2 : G), (v1, v2) ∈ edges G → v1 ∈ V1 ∨ v2 ∈ V1) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2) ∧ (∀ (v : G), ¬ (v ∈ V1 ∧ v ∈ V2)) ∧ (∀ (v : G), v ∈ V1 ∨ v ∈ V2 ∨ v ∉ G)), exists.intro V1 (exists.intro V2 (and.intro h (λ (v : G), or.inr (or.inr (or.elim (and.elim
end --Needs more than 2000 tokens!

--OUTPUT 6
theorem graph_bipartite_is_two_colorable (G : Type*) (E : set (G × G)) :
  (∀ x y : set G, ∀ e : G × G, e ∈ E → x ∈ e.1 ∧ y ∈ e.2 ∨ x ∈ e.2 ∧ y ∈ e.1) ↔
  (∃ c : G → Prop, ∀ v : G, c v ∨ ¬ c v ∧ ∀ e : G × G, e ∈ E → c e.1 ∧ ¬ c e.2 ∨ ¬ c e.1 ∧ c e.2) :=
begin
  split,
  assume h1 : ∀ x y : set G, ∀ e : G × G, e ∈ E → x ∈ e.1 ∧ y ∈ e.2 ∨ x ∈ e.2 ∧ y ∈ e.1,
  have h2 : ∃ c : G → Prop, ∀ v : G, c v ∨ ¬ c v, from by auto using [use (λ v : G, ∃ e : G × G, e ∈ E ∧ v ∈ e.1), exists_not_self, exists_not_self, exists.intro],
  have h3 : ∃ c : G → Prop, ∀ v : G, c v ∨ ¬ c v ∧ ∀ e : G × G, e ∈ E → c e.1 ∧ ¬ c e.2 ∨ ¬ c e.1 ∧ c e.2, from by auto [h2, h1],
  show ∃ c : G → Prop, ∀ v : G, c v ∨ ¬ c v ∧ ∀ e : G × G, e ∈ E → c e.1 ∧ ¬ c e.2 ∨ ¬ c e.1 ∧ c e.2, from h3,

  assume h1 : ∃ c : G → Prop, ∀ v : G, c v ∨ ¬ c v ∧ ∀ e : G × G, e ∈ E → c e.1 ∧ ¬ c e.2 ∨ ¬ c e.1 ∧ c e.2,
  have h2 : ∃ c : G → Prop, ∀ v : G, c v ∨ ¬ c v, from by auto [h1],
  have h3 : ∀ x y : set G, ∀ e : G × G, e ∈ E → x ∈ e.1 ∧ y ∈ e.2 ∨ x ∈ e.2 ∧ y ∈ e.1, from by auto [h2, h1],
  show ∀ x y : set G, ∀ e : G × G, e ∈ E → x ∈ e.1 ∧ y ∈ e.2 ∨ x ∈ e.2 ∧ y ∈ e.1, from h3,
end

--OUTPUT 7
theorem bipartite_two_colorable (G : Type*) [graph G] : two_colorable G ↔ bipartite G :=
begin
  have h1 : two_colorable G → bipartite G := λ h, begin
    have h2 : ∃ C : (vertex G → Prop) × (vertex G → Prop), ∀ v, (v ∈ C.1 ∨ v ∈ C.2) ∧ (∀ u w, edge G u w → v ∈ C.1 → (u ∈ C.1 ∧ w ∈ C.2) ∨ (u ∈ C.2 ∧ w ∈ C.1)), from by auto [h],
    have h3 : ∃ C : (vertex G → Prop) × (vertex G → Prop), ∀ v, (v ∈ C.1 ∨ v ∈ C.2) ∧ (∀ u w, edge G u w → (u ∈ C.1 ∧ w ∈ C.2) ∨ (u ∈ C.2 ∧ w ∈ C.1)), from by auto [h2],
    show bipartite G, from by auto [h3],
  end,
  have h2 : bipartite G → two_colorable G := λ h, begin
    have h3 : ∃ C : (vertex G → Prop) × (vertex G → Prop), ∀ v, (v ∈ C.1 ∨ v ∈ C.2) ∧ (∀ u w, edge G u w → (u ∈ C.1 ∧ w ∈ C.2) ∨ (u ∈ C.2 ∧ w ∈ C.1)), from by auto [h],
    have h4 : ∃ C : (vertex G → Prop) × (vertex G → Prop), ∀ v, (v ∈ C.1 ∨ v ∈ C.2) ∧ (∀ u w, edge G u w → v ∈ C.1 → (u ∈ C.1 ∧ w ∈ C.2) ∨ (u ∈ C.2 ∧ w ∈ C.1)), from by auto [h3],
    show two_colorable G, from by auto [h4],
  end,
  show two_colorable G ↔ bipartite G, from by auto [h1, h2],
end

--OUTPUT 8
theorem two_colorable_iff_is_bipartite (G : Type*) [graph G] : two_colorable G ↔ bipartite G :=
begin
  unfold two_colorable,
  split,
  {
    assume h1,
    unfold bipartite,
    use (λ x : G, red x ∨ blue x),
    use (λ x : G, red x → blue x),
    use (λ x : G, blue x → red x),
    split,
    {
      assume x y,
      assume h2,
      have h3 : red x ∨ blue x, from h1 x,
      have h4 : red y ∨ blue y, from h1 y,
      have h5 : (red x → blue x), from h1 x,
      have h6 : (blue x → red x), from h1 x,
      have h7 : (red y → blue y), from h1 y,
      have h8 : (blue y → red y), from h1 y,
      have h9 : (red x → blue y ∨ blue y → red x), from or.inr (by auto [h7, h5]),
      have h10 : (blue x → red y ∨ red y → blue x), from or.inr (by auto [h8, h6]),
      have h11 : (red x → blue y ∨ red y → blue x), from by auto [h9, h10],
      show (red x → blue y) ∨ (blue x → red y), from by auto [h11],
    },
    {
      assume x y,
      assume h2,
      have h3 : red x ∨ blue x, from h1 x,
      have h4 : red y ∨ blue y, from h1 y,
      have h5 : (red x → blue x), from h1 x,
      have h6 : (blue x → red x), from h1 x,
      have h7 : (red y → blue y), from h1 y,
      have h8 : (blue y → red y), from h1 y,
      have h9 : (red x → blue y ∨ blue y → red x), from or.inr (by auto [h7, h5]),
      have h10 : (blue x → red y ∨ red y → blue x), from or.inr (by auto [h8, h6]),
      have h11 : (red x → blue y ∨ red y → blue x), from by auto [h9, h10],
      show (blue y → red x) ∨ (red y → blue x), from by auto [h11],
    },
  },
  {
    assume h1,
    unfold bipartite at h1,
    cases h1 with f h1,
    cases h1 with g h1,
    cases h1 with h h1,
    cases h1 with h2 h3,
    use f,
    assume x,
    have h4 : f x = red x ∨ f x = blue x, from by auto [f],
    have h5 : f x = red x → g x = blue x, from by auto [h2 x],
    have h6 : f x = blue x → g x = red x, from by auto [h3 x],
    have h7 : f x = red x → g x = blue x ∨ f x = blue x → g x = red x, from or.inl (by auto [h5]),
    have h8 : f x = blue x → g x = red x ∨ f x = red x → g x = blue x, from or.inr (by auto [h6]),
    have h9 : f x = red x → g x = blue x ∨ f x = blue x → g x = red x, from by auto [h7, h8],
    show f x → g x, from by auto [h9],
  },
end

/- FEW SHOT PROMPTS TO CODEX(START)
/--`theorem`
Power Set is Closed under Intersection
Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:
:$\forall A, B \in \powerset S: A \cap B \in \powerset S$
`proof`
Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.
{{qed}}
-/
theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈ 𝒫 S, (A ∩ B) ∈ 𝒫 S :=
begin
  assume (A : set α) (hA : A ∈ 𝒫 S) (B : set α) (hB : B ∈ 𝒫 S),
  have h1 : (A ⊆ S) ∧ (B ⊆ S), from by auto [set.subset_of_mem_powerset, set.subset_of_mem_powerset],
  have h2 : (A ∩ B) ⊆ A, from by auto [set.inter_subset_left],
  have h3 : (A ∩ B) ⊆ S, from by auto [set.subset.trans],
  show (A ∩ B) ∈  𝒫 S, from by auto [set.mem_powerset],
end

/--`theorem`
Square of Sum
 :$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$
`proof`
Follows from the distribution of multiplication over addition:

{{begin-eqn}}
{{eqn | l = \left({x + y}\right)^2
      | r = \left({x + y}\right) \cdot \left({x + y}\right)
}}
{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x^2 + 2xy + y^2
      | c =
}}
{{end-eqn}}
{{qed}}
-/
theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2) :=
begin
  calc (x + y)^2 = (x+y)*(x+y) : by auto [sq]
  ... = x*(x+y) + y*(x+y) : by auto [add_mul]
  ... = x*x + x*y + y*x + y*y : by auto [mul_comm, add_mul] using [ring]
  ... = x^2 + 2*x*y + y^2 : by auto [sq, mul_comm] using [ring]
end

/--`theorem`
Identity of Group is Unique
Let $\struct {G, \circ}$ be a group. Then there is a unique identity element $e \in G$.
`proof`
From Group has Latin Square Property, there exists a unique $x \in G$ such that:
:$a x = b$

and there exists a unique $y \in G$ such that:
:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:
:$a x = a$

and there exists a unique $y \in G$ such that:
:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.
{{qed}}
-/
theorem group_identity_unique {G : Type*} [group G] : ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a :=
begin
  have h1 : ∀ a b : G, ∃! x : G, a * x = b, from by auto using [use (a⁻¹ * b)],
  have h2 : ∀ a b : G, ∃! y : G, y * a = b, from by auto using [use b * a⁻¹],

  have h3 : ∀ a : G, ∃! x : G, a * x = a, from by auto [h1],
  have h4 : ∀ a : G, ∃! y : G, y * a = a, from by auto [h2],

  have h5 : ∀ a : G, classical.some (h3 a).exists = (1 : G), from by auto [exists_unique.unique, h3, classical.some_spec, exists_unique.exists, mul_one],
  have h6 : ∀ a : G, classical.some (h4 a).exists = (1 : G), from by auto [exists_unique.unique, h4, classical.some_spec, exists_unique.exists, one_mul],

  show ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a, from by auto [h3, h4, exists_unique.unique, classical.some_spec, exists_unique.exists] using [use (1 : G)],
end

/--`theorem`
Bipartite Graph is two colorable
Let $G$ be a graph. Then $G$ is 2-colorable if and only if $G$ is bipartite.
`proof`
Let $G$ be a 2-colorable graph, which means we can color every vertex either red or blue, and no edge will have both endpoints colored the same color. Let $A$ denote the subset of vertices colored red, and let $B$ denote the subset of vertices colored blue. Since all vertices of $A$ are red, there are no edges within $A$, and similarly for $B$. This implies that every edge has one endpoint in $A$ and the other in $B$, which means $G$ is bipartite.

Conversely, suppose $G$ is bipartite, that is, we can partition the vertices into two subsets $V_{1}, V_{2}$ every edge has one endpoint in $V_{1}$ and the other in $V_{2}$. Then coloring every vertex of $V_{1}$ red and every vertex of $V_{2}$ blue yields a valid coloring, so $G$ is 2-colorable.

QED

-/
theorem
FEW SHOT PROMPTS TO CODEX(END)-/


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
-/
import data.polynomial.reverse
import algebra.regular.smul

/-!
# Theory of monic polynomials

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

We give several tools for proving that polynomials are monic, e.g.
`monic.mul`, `monic.map`, `monic.pow`.
-/

noncomputable theory

open finset
open_locale big_operators classical polynomial

namespace polynomial
universes u v y
variables {R : Type u} {S : Type v} {a b : R} {m n : ℕ} {ι : Type y}

section semiring
variables [semiring R] {p q r : R[X]}

lemma monic_zero_iff_subsingleton : monic (0 : R[X]) ↔ subsingleton R :=
subsingleton_iff_zero_eq_one

lemma not_monic_zero_iff : ¬ monic (0 : R[X]) ↔ (0 : R) ≠ 1 :=
(monic_zero_iff_subsingleton.trans subsingleton_iff_zero_eq_one.symm).not

lemma monic_zero_iff_subsingleton' :
  monic (0 : R[X]) ↔ (∀ f g : R[X], f = g) ∧ (∀ a b : R, a = b) :=
polynomial.monic_zero_iff_subsingleton.trans ⟨by { introI, simp },
  λ h, subsingleton_iff.mpr h.2⟩

lemma monic.as_sum (hp : p.monic) :
  p = X^(p.nat_degree) + (∑ i in range p.nat_degree, C (p.coeff i) * X^i) :=
begin
  conv_lhs { rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm] },
  suffices : C (p.coeff p.nat_degree) = 1,
  { rw [this, one_mul] },
  exact congr_arg C hp
end

lemma ne_zero_of_ne_zero_of_monic (hp : p ≠ 0) (hq : monic q) : q ≠ 0 :=
begin
  rintro rfl,
  rw [monic.def, leading_coeff_zero] at hq,
  rw [← mul_one p, ← C_1, ← hq, C_0, mul_zero] at hp,
  exact hp rfl
end

lemma monic.map [semiring S] (f : R →+* S) (hp : monic p) : monic (p.map f) :=
begin
  nontriviality,
  have : f (leading_coeff p) ≠ 0,
  { rw [show _ = _, from hp, f.map_one],
    exact one_ne_zero, },
  rw [monic, leading_coeff, coeff_map],
  suffices : p.coeff (map f p).nat_degree = 1,
  { simp [this], },
  rwa nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f this),
end

lemma monic_C_mul_of_mul_leading_coeff_eq_one {b : R} (hp : b * p.leading_coeff = 1) :
  monic (C b * p) :=
by { nontriviality, rw [monic, leading_coeff_mul' _]; simp [leading_coeff_C b, hp] }

lemma monic_mul_C_of_leading_coeff_mul_eq_one {b : R} (hp : p.leading_coeff * b = 1) :
  monic (p * C b) :=
by { nontriviality, rw [monic, leading_coeff_mul' _]; simp [leading_coeff_C b, hp] }

theorem monic_of_degree_le (n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1) : monic p :=
decidable.by_cases
  (assume H : degree p < n, eq_of_zero_eq_one
    (H2 ▸ (coeff_eq_zero_of_degree_lt H).symm) _ _)
  (assume H : ¬degree p < n,
    by rwa [monic, leading_coeff, nat_degree, (lt_or_eq_of_le H1).resolve_left H])

theorem monic_X_pow_add {n : ℕ} (H : degree p ≤ n) : monic (X ^ (n+1) + p) :=
have H1 : degree p < n+1, from lt_of_le_of_lt H (with_bot.coe_lt_coe.2 (nat.lt_succ_self n)),
monic_of_degree_le (n+1)
  (le_trans (degree_add_le _ _) (max_le (degree_X_pow_le _) (le_of_lt H1)))
  (by rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H1, add_zero])

theorem monic_X_add_C (x : R) : monic (X + C x) :=
pow_one (X : R[X]) ▸ monic_X_pow_add degree_C_le

lemma monic.mul (hp : monic p) (hq : monic q) : monic (p * q) :=
if h0 : (0 : R) = 1 then by haveI := subsingleton_of_zero_eq_one h0;
  exact subsingleton.elim _ _
else
  have leading_coeff p * leading_coeff q ≠ 0, by simp [monic.def.1 hp, monic.def.1 hq, ne.symm h0],
  by rw [monic.def, leading_coeff_mul' this, monic.def.1 hp, monic.def.1 hq, one_mul]

lemma monic.pow (hp : monic p) : ∀ (n : ℕ), monic (p ^ n)
| 0     := monic_one
| (n+1) := by { rw pow_succ, exact hp.mul (monic.pow n) }

lemma monic.add_of_left (hp : monic p) (hpq : degree q < degree p) :
  monic (p + q) :=
by rwa [monic, add_comm, leading_coeff_add_of_degree_lt hpq]

lemma monic.add_of_right (hq : monic q) (hpq : degree p < degree q) :
  monic (p + q) :=
by rwa [monic, leading_coeff_add_of_degree_lt hpq]

lemma monic.of_mul_monic_left (hp : p.monic) (hpq : (p * q).monic) : q.monic :=
begin
  contrapose! hpq,
  rw monic.def at hpq ⊢,
  rwa leading_coeff_monic_mul hp,
end

lemma monic.of_mul_monic_right (hq : q.monic) (hpq : (p * q).monic) : p.monic :=
begin
  contrapose! hpq,
  rw monic.def at hpq ⊢,
  rwa leading_coeff_mul_monic hq,
end

namespace monic

@[simp]
lemma nat_degree_eq_zero_iff_eq_one (hp : p.monic) :
  p.nat_degree = 0 ↔ p = 1 :=
begin
  split; intro h,
  swap, { rw h, exact nat_degree_one },
  have : p = C (p.coeff 0),
  { rw ← polynomial.degree_le_zero_iff,
    rwa polynomial.nat_degree_eq_zero_iff_degree_le_zero at h },
  rw this, convert C_1, rw ← h, apply hp,
end

@[simp]
lemma degree_le_zero_iff_eq_one (hp : p.monic) :
  p.degree ≤ 0 ↔ p = 1 :=
by rw [←hp.nat_degree_eq_zero_iff_eq_one, nat_degree_eq_zero_iff_degree_le_zero]

lemma nat_degree_mul (hp : p.monic) (hq : q.monic) :
  (p * q).nat_degree = p.nat_degree + q.nat_degree :=
begin
  nontriviality R,
  apply nat_degree_mul',
  simp [hp.leading_coeff, hq.leading_coeff]
end

lemma degree_mul_comm (hp : p.monic) (q : R[X]) :
  (p * q).degree = (q * p).degree :=
begin
  by_cases h : q = 0,
  { simp [h] },
  rw [degree_mul', hp.degree_mul],
  { exact add_comm _ _ },
  { rwa [hp.leading_coeff, one_mul, leading_coeff_ne_zero] }
end

lemma nat_degree_mul' (hp : p.monic) (hq : q ≠ 0) :
  (p * q).nat_degree = p.nat_degree + q.nat_degree :=
begin
  rw [nat_degree_mul', add_comm],
  simpa [hp.leading_coeff, leading_coeff_ne_zero]
end

lemma nat_degree_mul_comm (hp : p.monic) (q : R[X]) :
  (p * q).nat_degree = (q * p).nat_degree :=
begin
  by_cases h : q = 0,
  { simp [h] },
  rw [hp.nat_degree_mul' h, polynomial.nat_degree_mul', add_comm],
  simpa [hp.leading_coeff, leading_coeff_ne_zero]
end

lemma not_dvd_of_nat_degree_lt (hp : monic p)
  (h0 : q ≠ 0) (hl : nat_degree q < nat_degree p) : ¬ p ∣ q :=
begin
  rintro ⟨r, rfl⟩,
  rw [hp.nat_degree_mul' $ right_ne_zero_of_mul h0] at hl,
  exact hl.not_le (nat.le_add_right _ _)
end

lemma not_dvd_of_degree_lt (hp : monic p)
  (h0 : q ≠ 0) (hl : degree q < degree p) : ¬ p ∣ q :=
monic.not_dvd_of_nat_degree_lt hp h0 $ nat_degree_lt_nat_degree h0 hl

lemma next_coeff_mul (hp : monic p) (hq : monic q) :
  next_coeff (p * q) = next_coeff p + next_coeff q :=
begin
  nontriviality,
  simp only [← coeff_one_reverse],
  rw reverse_mul;
    simp [coeff_mul, nat.antidiagonal, hp.leading_coeff, hq.leading_coeff, add_comm]
end

lemma eq_one_of_map_eq_one {S : Type*} [semiring S] [nontrivial S]
  (f : R →+* S) (hp : p.monic) (map_eq : p.map f = 1) : p = 1 :=
begin
  nontriviality R,
  have hdeg : p.degree = 0,
  { rw [← degree_map_eq_of_leading_coeff_ne_zero f _, map_eq, degree_one],
    { rw [hp.leading_coeff, f.map_one],
      exact one_ne_zero } },
  have hndeg : p.nat_degree = 0 :=
    with_bot.coe_eq_coe.mp ((degree_eq_nat_degree hp.ne_zero).symm.trans hdeg),
  convert eq_C_of_degree_eq_zero hdeg,
  rw [← hndeg, ← polynomial.leading_coeff, hp.leading_coeff, C.map_one]
end

lemma nat_degree_pow (hp : p.monic) (n : ℕ) :
  (p ^ n).nat_degree = n * p.nat_degree :=
begin
  induction n with n hn,
  { simp },
  { rw [pow_succ, hp.nat_degree_mul (hp.pow n), hn],
    ring }
end

end monic

@[simp] lemma nat_degree_pow_X_add_C [nontrivial R] (n : ℕ) (r : R) :
  ((X + C r) ^ n).nat_degree = n :=
by rw [(monic_X_add_C r).nat_degree_pow, nat_degree_X_add_C, mul_one]

lemma monic.eq_one_of_is_unit (hm : monic p) (hpu : is_unit p) : p = 1 :=
begin
  nontriviality R,
  obtain ⟨q, h⟩ := hpu.exists_right_inv,
  have := hm.nat_degree_mul' (right_ne_zero_of_mul_eq_one h),
  rw [h, nat_degree_one, eq_comm, add_eq_zero_iff] at this,
  exact hm.nat_degree_eq_zero_iff_eq_one.mp this.1,
end

lemma monic.is_unit_iff (hm : p.monic) : is_unit p ↔ p = 1 :=
⟨hm.eq_one_of_is_unit, λ h, h.symm ▸ is_unit_one⟩

end semiring

section comm_semiring
variables [comm_semiring R] {p : R[X]}

lemma monic_multiset_prod_of_monic (t : multiset ι) (f : ι → R[X])
  (ht : ∀ i ∈ t, monic (f i)) :
  monic (t.map f).prod :=
begin
  revert ht,
  refine t.induction_on _ _, { simp },
  intros a t ih ht,
  rw [multiset.map_cons, multiset.prod_cons],
  exact (ht _ (multiset.mem_cons_self _ _)).mul (ih (λ _ hi, ht _ (multiset.mem_cons_of_mem hi)))
end

lemma monic_prod_of_monic (s : finset ι) (f : ι → R[X]) (hs : ∀ i ∈ s, monic (f i)) :
  monic (∏ i in s, f i) :=
monic_multiset_prod_of_monic s.1 f hs

lemma monic.next_coeff_multiset_prod (t : multiset ι) (f : ι → R[X])
  (h : ∀ i ∈ t, monic (f i)) :
  next_coeff (t.map f).prod = (t.map (λ i, next_coeff (f i))).sum :=
begin
  revert h,
  refine multiset.induction_on t _ (λ a t ih ht, _),
  { simp only [multiset.not_mem_zero, forall_prop_of_true, forall_prop_of_false, multiset.map_zero,
               multiset.prod_zero, multiset.sum_zero, not_false_iff, forall_true_iff],
    rw ← C_1, rw next_coeff_C_eq_zero },
  { rw [multiset.map_cons, multiset.prod_cons, multiset.map_cons, multiset.sum_cons,
        monic.next_coeff_mul, ih],
    exacts [λ i hi, ht i (multiset.mem_cons_of_mem hi), ht a (multiset.mem_cons_self _ _),
            monic_multiset_prod_of_monic _ _ (λ b bs, ht _ (multiset.mem_cons_of_mem bs))] }
end

lemma monic.next_coeff_prod (s : finset ι) (f : ι → R[X]) (h : ∀ i ∈ s, monic (f i)) :
  next_coeff (∏ i in s, f i) = ∑ i in s, next_coeff (f i) :=
monic.next_coeff_multiset_prod s.1 f h

end comm_semiring

section semiring
variables [semiring R]

@[simp]
lemma monic.nat_degree_map [semiring S] [nontrivial S] {P : R[X]} (hmo : P.monic)
  (f : R →+* S) : (P.map f).nat_degree = P.nat_degree :=
begin
  refine le_antisymm (nat_degree_map_le _ _) (le_nat_degree_of_ne_zero _),
  rw [coeff_map, monic.coeff_nat_degree hmo, ring_hom.map_one],
  exact one_ne_zero
end

@[simp]
lemma monic.degree_map [semiring S] [nontrivial S] {P : R[X]} (hmo : P.monic)
  (f : R →+* S) : (P.map f).degree = P.degree :=
begin
  by_cases hP : P = 0,
  { simp [hP] },
  { refine le_antisymm (degree_map_le _ _) _,
    rw [degree_eq_nat_degree hP],
    refine le_degree_of_ne_zero _,
    rw [coeff_map, monic.coeff_nat_degree hmo, ring_hom.map_one],
    exact one_ne_zero }
end

section injective
open function
variables [semiring S] {f : R →+* S} (hf : injective f)
include hf

lemma degree_map_eq_of_injective (p : R[X]) : degree (p.map f) = degree p :=
if h : p = 0 then by simp [h]
else degree_map_eq_of_leading_coeff_ne_zero _
  (by rw [← f.map_zero]; exact mt hf.eq_iff.1
    (mt leading_coeff_eq_zero.1 h))

lemma nat_degree_map_eq_of_injective (p : R[X]) :
  nat_degree (p.map f) = nat_degree p :=
nat_degree_eq_of_degree_eq (degree_map_eq_of_injective hf p)

lemma leading_coeff_map' (p : R[X]) :
  leading_coeff (p.map f) = f (leading_coeff p) :=
begin
  unfold leading_coeff,
  rw [coeff_map, nat_degree_map_eq_of_injective hf p],
end

lemma next_coeff_map (p : R[X]) :
  (p.map f).next_coeff = f p.next_coeff :=
begin
  unfold next_coeff,
  rw nat_degree_map_eq_of_injective hf,
  split_ifs; simp
end

lemma leading_coeff_of_injective (p : R[X]) :
  leading_coeff (p.map f) = f (leading_coeff p) :=
begin
  delta leading_coeff,
  rw [coeff_map f, nat_degree_map_eq_of_injective hf p]
end

lemma monic_of_injective {p : R[X]} (hp : (p.map f).monic) : p.monic :=
begin
  apply hf,
  rw [← leading_coeff_of_injective hf, hp.leading_coeff, f.map_one]
end

theorem _root_.function.injective.monic_map_iff {p : R[X]} : p.monic ↔ (p.map f).monic :=
⟨monic.map _, polynomial.monic_of_injective hf⟩

end injective

end semiring

section ring
variables [ring R] {p : R[X]}

theorem monic_X_sub_C (x : R) : monic (X - C x) :=
by simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)

theorem monic_X_pow_sub {n : ℕ} (H : degree p ≤ n) : monic (X ^ (n+1) - p) :=
by simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) ≤ n, by rwa ←degree_neg p at H)

/-- `X ^ n - a` is monic. -/
lemma monic_X_pow_sub_C {R : Type u} [ring R] (a : R) {n : ℕ} (h : n ≠ 0) : (X ^ n - C a).monic :=
begin
  obtain ⟨k, hk⟩ := nat.exists_eq_succ_of_ne_zero h,
  convert monic_X_pow_sub _,
  exact le_trans degree_C_le nat.with_bot.coe_nonneg,
end

lemma not_is_unit_X_pow_sub_one (R : Type*) [comm_ring R] [nontrivial R] (n : ℕ) :
  ¬ is_unit (X ^ n - 1 : R[X]) :=
begin
  intro h,
  rcases eq_or_ne n 0 with rfl | hn,
  { simpa using h },
  apply hn,
  rw [←@nat_degree_one R, ←(monic_X_pow_sub_C _ hn).eq_one_of_is_unit h, nat_degree_X_pow_sub_C],
end

lemma monic.sub_of_left {p q : R[X]} (hp : monic p) (hpq : degree q < degree p) :
  monic (p - q) :=
by { rw sub_eq_add_neg, apply hp.add_of_left, rwa degree_neg }

lemma monic.sub_of_right {p q : R[X]}
  (hq : q.leading_coeff = -1) (hpq : degree p < degree q) : monic (p - q) :=
have (-q).coeff (-q).nat_degree = 1 :=
by rw [nat_degree_neg, coeff_neg, show q.coeff q.nat_degree = -1, from hq, neg_neg],
by { rw sub_eq_add_neg, apply monic.add_of_right this, rwa degree_neg }

end ring

section nonzero_semiring
variables [semiring R] [nontrivial R] {p q : R[X]}

@[simp] lemma not_monic_zero : ¬monic (0 : R[X]) :=
not_monic_zero_iff.mp zero_ne_one

end nonzero_semiring

section not_zero_divisor

-- TODO: using gh-8537, rephrase lemmas that involve commutation around `*` using the op-ring

variables [semiring R] {p : R[X]}

lemma monic.mul_left_ne_zero (hp : monic p) {q : R[X]} (hq : q ≠ 0) :
  q * p ≠ 0 :=
begin
  by_cases h : p = 1,
  { simpa [h] },
  rw [ne.def, ←degree_eq_bot, hp.degree_mul, with_bot.add_eq_bot, not_or_distrib, degree_eq_bot],
  refine ⟨hq, _⟩,
  rw [←hp.degree_le_zero_iff_eq_one, not_le] at h,
  refine (lt_trans _ h).ne',
  simp
end

lemma monic.mul_right_ne_zero (hp : monic p) {q : R[X]} (hq : q ≠ 0) :
  p * q ≠ 0 :=
begin
  by_cases h : p = 1,
  { simpa [h] },
  rw [ne.def, ←degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, with_bot.add_eq_bot,
      not_or_distrib, degree_eq_bot],
  refine ⟨hq, _⟩,
  rw [←hp.degree_le_zero_iff_eq_one, not_le] at h,
  refine (lt_trans _ h).ne',
  simp
end

lemma monic.mul_nat_degree_lt_iff (h : monic p) {q : R[X]} :
  (p * q).nat_degree < p.nat_degree ↔ p ≠ 1 ∧ q = 0 :=
begin
  by_cases hq : q = 0,
  { suffices : 0 < p.nat_degree ↔ p.nat_degree ≠ 0,
    { simpa [hq, ←h.nat_degree_eq_zero_iff_eq_one] },
    exact ⟨λ h, h.ne', λ h, lt_of_le_of_ne (nat.zero_le _) h.symm ⟩ },
  { simp [h.nat_degree_mul', hq] }
end

lemma monic.mul_right_eq_zero_iff (h : monic p) {q : R[X]} :
  p * q = 0 ↔ q = 0 :=
begin
  by_cases hq : q = 0;
  simp [h.mul_right_ne_zero, hq]
end

lemma monic.mul_left_eq_zero_iff (h : monic p) {q : R[X]} :
  q * p = 0 ↔ q = 0 :=
begin
  by_cases hq : q = 0;
  simp [h.mul_left_ne_zero, hq]
end

lemma monic.is_regular {R : Type*} [ring R] {p : R[X]} (hp : monic p) : is_regular p :=
begin
  split,
  { intros q r h,
    rw [←sub_eq_zero, ←hp.mul_right_eq_zero_iff, mul_sub, h, sub_self] },
  { intros q r h,
    simp only at h,
    rw [←sub_eq_zero, ←hp.mul_left_eq_zero_iff, sub_mul, h, sub_self] }
end

lemma degree_smul_of_smul_regular {S : Type*} [monoid S] [distrib_mul_action S R]
  {k : S} (p : R[X]) (h : is_smul_regular R k) :
  (k • p).degree = p.degree :=
begin
  refine le_antisymm _ _,
  { rw degree_le_iff_coeff_zero,
    intros m hm,
    rw degree_lt_iff_coeff_zero at hm,
    simp [hm m le_rfl] },
  { rw degree_le_iff_coeff_zero,
    intros m hm,
    rw degree_lt_iff_coeff_zero at hm,
    refine h _,
    simpa using hm m le_rfl },
end

lemma nat_degree_smul_of_smul_regular {S : Type*} [monoid S] [distrib_mul_action S R]
  {k : S} (p : R[X]) (h : is_smul_regular R k) :
  (k • p).nat_degree = p.nat_degree :=
begin
  by_cases hp : p = 0,
  { simp [hp] },
  rw [←with_bot.coe_eq_coe, ←degree_eq_nat_degree hp, ←degree_eq_nat_degree,
      degree_smul_of_smul_regular p h],
  contrapose! hp,
  rw ←smul_zero k at hp,
  exact h.polynomial hp
end

lemma leading_coeff_smul_of_smul_regular {S : Type*} [monoid S] [distrib_mul_action S R]
  {k : S} (p : R[X]) (h : is_smul_regular R k) :
  (k • p).leading_coeff = k • p.leading_coeff :=
by rw [leading_coeff, leading_coeff, coeff_smul, nat_degree_smul_of_smul_regular p h]

lemma monic_of_is_unit_leading_coeff_inv_smul (h : is_unit p.leading_coeff) :
  monic (h.unit⁻¹ • p) :=
begin
  rw [monic.def, leading_coeff_smul_of_smul_regular _ (is_smul_regular_of_group _), units.smul_def],
  obtain ⟨k, hk⟩ := h,
  simp only [←hk, smul_eq_mul, ←units.coe_mul, units.coe_eq_one, inv_mul_eq_iff_eq_mul],
  simp [units.ext_iff, is_unit.unit_spec]
end

lemma is_unit_leading_coeff_mul_right_eq_zero_iff (h : is_unit p.leading_coeff) {q : R[X]} :
  p * q = 0 ↔ q = 0 :=
begin
  split,
  { intro hp,
    rw ←smul_eq_zero_iff_eq (h.unit)⁻¹ at hp,
    have : (h.unit)⁻¹ • (p * q) = ((h.unit)⁻¹ • p) * q,
    { ext,
      simp only [units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum],
      refine sum_congr rfl (λ x hx, _),
      rw ←mul_assoc },
    rwa [this, monic.mul_right_eq_zero_iff] at hp,
    exact monic_of_is_unit_leading_coeff_inv_smul _ },
  { rintro rfl,
    simp }
end

end not_zero_divisor

end polynomial

repo: mathlib


text:
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
-/
import topology.algebra.ordered.basic
import topology.extend_from

/-!
# Lemmas about `extend_from` in an order topology.
-/

open filter set topological_space
open_locale topological_space classical

universes u v
variables {α : Type u} {β : Type v}

lemma continuous_on_Icc_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
  [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α}
  {la lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
  (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
  continuous_on (extend_from (Ioo a b) f) (Icc a b) :=
begin
  apply continuous_on_extend_from,
  { rw closure_Ioo hab, },
  { intros x x_in,
    rcases mem_Ioo_or_eq_endpoints_of_mem_Icc x_in with rfl | rfl | h,
    { use la,
      simpa [hab] },
    { use lb,
      simpa [hab] },
    { use [f x, hf x h] } }
end

lemma eq_lim_at_left_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
  [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α}
  {la : β} (hab : a < b) (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) :
  extend_from (Ioo a b) f a = la :=
begin
  apply extend_from_eq,
  { rw closure_Ioo hab,
    simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
  { simpa [hab] }
end

lemma eq_lim_at_right_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
  [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α}
  {lb : β} (hab : a < b) (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
  extend_from (Ioo a b) f b = lb :=
begin
  apply extend_from_eq,
  { rw closure_Ioo hab,
    simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
  { simpa [hab] }
end

lemma continuous_on_Ico_extend_from_Ioo [topological_space α]
  [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
  [regular_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
  (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) :
  continuous_on (extend_from (Ioo a b) f) (Ico a b) :=
begin
  apply continuous_on_extend_from,
  { rw [closure_Ioo hab], exact Ico_subset_Icc_self, },
  { intros x x_in,
    rcases mem_Ioo_or_eq_left_of_mem_Ico x_in with rfl | h,
    { use la,
      simpa [hab] },
    { use [f x, hf x h] } }
end

lemma continuous_on_Ioc_extend_from_Ioo [topological_space α]
  [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
  [regular_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
  (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
  continuous_on (extend_from (Ioo a b) f) (Ioc a b) :=
begin
  have := @continuous_on_Ico_extend_from_Ioo (order_dual α) _ _ _ _ _ _ _ f _ _ _ hab,
  erw [dual_Ico, dual_Ioi, dual_Ioo] at this,
  exact this hf hb
end


text:
-- ---------------------------------------------------------------------
-- Ejercicio. Importar la librería de tácticas
-- ----------------------------------------------------------------------

import tactic

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
--    ¬ ¬ P → P
-- ----------------------------------------------------------------------

-- 1ª demostración
-- ===============

example (P : Prop) : ¬ ¬ P → P :=
begin
  intro h,
  cases classical.em P,
  { assumption },
  { contradiction },
end

-- Prueba
-- ======

/-
P : Prop
⊢ ¬¬P → P
  >> intro h,
h : ¬¬P
⊢ P
  >> cases classical.em P,
| h : ¬¬P
| ⊢ P
|   >> { assumption },
h_1 : ¬P
⊢ P
  >> { contradiction },
no goals
-/

-- 2ª demostración
-- ===============

open classical

example (P : Prop) : ¬ ¬ P → P :=
begin
  intro h,
  cases classical.em P,
  { assumption },
  { contradiction },
end

-- 3ª demostración
-- ===============

open_locale classical

example (P : Prop) : ¬ ¬ P → P :=
begin
  intro h,
  by_cases h' : P,
  { assumption },
  { contradiction },
end

-- Prueba
-- ======

/-
P : Prop
⊢ ¬¬P → P
  >> intro h,
h : ¬¬P
⊢ P
  >> by_cases h' : P,
| 2 goals
| P : Prop,
| h : ¬¬P,
| h' : P
| ⊢ P
|   >> { assumption },
h' : ¬P
⊢ P
  >> { contradiction },
no goals
-/

author: jaalonso


text:
-- Identidad_de_Brahmagupta-Fibonacci.lean
-- Identidad de Brahmagupta-Fibonacci
-- José A. Alonso Jiménez
-- Sevilla, 26 de septiembre de 2021
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Demostrar la identidad de Brahmagupta-Fibonacci https://bit.ly/3ucEc80
--    (a² + b²) * (c² + d²) = (ac - bd)² + (ad + bc)²
-- ---------------------------------------------------------------------

import data.real.basic

variables (a b c d : ℝ)

-- 1ª demostración
example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
calc (a^2 + b^2) * (c^2 + d^2)
     = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)
         : right_distrib (a^2) (b^2) (c^2 + d^2)
 ... = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)
         : congr_arg2 (+) (left_distrib (a^2) (c^2) (d^2)) rfl
 ... = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)
         : congr_arg2 (+) rfl (left_distrib (b^2) (c^2) (d^2))
 ... = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)
         : by ring
 ... = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)
         : by ring
 ... = (a*c - b*d)^2 + (a*d + b*c)^2
         : by ring

-- 2ª demostración
example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
by ring

repo: Calculemus

save_path: github-repos/lean/jaalonso-Calculemus