Merge remote-tracking branch 'upstream/master' into bump/v4.27.0

Author: kim-em

Mathlib.lean

@@ -1561,6 +1561,7 @@ public import Mathlib.Analysis.Calculus.FDeriv.Comp
 public import Mathlib.Analysis.Calculus.FDeriv.CompCLM
 public import Mathlib.Analysis.Calculus.FDeriv.Congr
 public import Mathlib.Analysis.Calculus.FDeriv.Const
+public import Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
 public import Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
 public import Mathlib.Analysis.Calculus.FDeriv.Defs
 public import Mathlib.Analysis.Calculus.FDeriv.Equiv
@@ -2065,6 +2066,7 @@ public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Pos
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
+public import Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
 public import Mathlib.Analysis.SpecialFunctions.Exp
 public import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 public import Mathlib.Analysis.SpecialFunctions.Exponential
@@ -2876,6 +2878,7 @@ public import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
 public import Mathlib.CategoryTheory.Presentable.Basic
 public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
 public import Mathlib.CategoryTheory.Presentable.ColimitPresentation
+public import Mathlib.CategoryTheory.Presentable.Dense
 public import Mathlib.CategoryTheory.Presentable.Finite
 public import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
 public import Mathlib.CategoryTheory.Presentable.Limits
@@ -3211,6 +3214,11 @@ public import Mathlib.Combinatorics.SimpleGraph.Turan
 public import Mathlib.Combinatorics.SimpleGraph.Tutte
 public import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
 public import Mathlib.Combinatorics.SimpleGraph.Walk
+public import Mathlib.Combinatorics.SimpleGraph.Walks.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Walks.Maps
+public import Mathlib.Combinatorics.SimpleGraph.Walks.Operations
+public import Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks
+public import Mathlib.Combinatorics.SimpleGraph.Walks.Traversal
 public import Mathlib.Combinatorics.Young.SemistandardTableau
 public import Mathlib.Combinatorics.Young.YoungDiagram
 public import Mathlib.Computability.Ackermann
@@ -6553,7 +6561,6 @@ public import Mathlib.Tactic.Positivity.Basic
 public import Mathlib.Tactic.Positivity.Core
 public import Mathlib.Tactic.Positivity.Finset
 public import Mathlib.Tactic.ProdAssoc
-public import Mathlib.Tactic.Propose
 public import Mathlib.Tactic.ProxyType
 public import Mathlib.Tactic.Push
 public import Mathlib.Tactic.Push.Attr

Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

@@ -628,6 +628,9 @@ lemma map_eq_natCast_iff {f : β → α} {n : ℕ} {a : WithBot β} :
 lemma natCast_eq_map_iff {f : β → α} {n : ℕ} {a : WithBot β} :
     n = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
 
+@[simp] lemma bot_lt_natCast [LT α] (n : ℕ) : (⊥ : WithBot α) < n :=
+  WithBot.bot_lt_coe _
+
 end AddMonoidWithOne
 
 instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithBot α) :=

Mathlib/Algebra/Polynomial/Factors.lean

@@ -6,6 +6,7 @@ Authors: Thomas Browning
 module
 
 public import Mathlib.Algebra.Polynomial.FieldDivision
+public import Mathlib.Algebra.Polynomial.Taylor
 
 /-!
 # Split polynomials
@@ -106,6 +107,10 @@ protected theorem Splits.prod {ι : Type*} {f : ι → R[X]} {s : Finset ι}
     (h : ∀ i ∈ s, Splits (f i)) : Splits (∏ i ∈ s, f i) :=
   prod_mem h
 
+lemma Splits.taylor {p : R[X]} (hp : p.Splits) (r : R) : (p.taylor r).Splits := by
+  have (i : _) : (X + C r + C i).Splits := by simpa [add_assoc] using Splits.X_add_C (r + i)
+  induction hp using Submonoid.closure_induction <;> aesop
+
 /-- See `splits_iff_exists_multiset` for the version with subtraction. -/
 theorem splits_iff_exists_multiset' {f : R[X]} :
     Splits f ↔ ∃ m : Multiset R, f = C f.leadingCoeff * (m.map (X + C ·)).prod := by
@@ -246,6 +251,23 @@ theorem Splits.splits (hf : Splits f) :
   or_iff_not_imp_left.mpr fun hf0 _ hg hgf ↦ degree_le_of_natDegree_le <|
     (hf.of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg
 
+lemma map_sub_sprod_roots_eq_prod_map_eval
+    (s : Multiset R) (g : R[X]) (hg : g.Monic) (hg' : g.Splits) :
+    ((s ×ˢ g.roots).map fun ij ↦ ij.1 - ij.2).prod = (s.map g.eval).prod := by
+  have := hg'.eq_prod_roots
+  rw [hg.leadingCoeff, map_one, one_mul] at this
+  conv_rhs => rw [this]
+  simp_rw [eval_multiset_prod, Multiset.prod_map_product_eq_prod_prod, Multiset.map_map]
+  congr! with x hx
+  ext; simp
+
+lemma map_sub_roots_sprod_eq_prod_map_eval
+    (s : Multiset R) (g : R[X]) (hg : g.Monic) (hg' : g.Splits) :
+    ((g.roots ×ˢ s).map fun ij ↦ ij.1 - ij.2).prod =
+      (-1) ^ (s.card * g.roots.card) * (s.map g.eval).prod := by
+  trans ((s ×ˢ g.roots).map fun ij ↦ (-1) * (ij.1 - ij.2)).prod
+  · rw [← Multiset.map_swap_product, Multiset.map_map]; simp
+  · rw [Multiset.prod_map_mul]; simp [map_sub_sprod_roots_eq_prod_map_eval _ _ hg hg']
 end CommRing
 
 section DivisionSemiring

Mathlib/Algebra/Polynomial/Taylor.lean

@@ -117,6 +117,10 @@ theorem eq_zero_of_hasseDeriv_eq_zero (f : R[X]) (r : R)
   ext k
   rw [taylor_coeff, h, coeff_zero]
 
+@[simp] lemma map_taylor {R S : Type*} [Semiring R] [Semiring S] (p : R[X]) (r : R) (f : R →+* S) :
+    (p.taylor r).map f = (p.map f).taylor (f r) := by
+  simp [taylor_apply, Polynomial.map_comp]
+
 end Semiring
 
 section Ring

Mathlib/Analysis/Asymptotics/TVS.lean

@@ -305,6 +305,18 @@ lemma _root_.ContinuousLinearMap.isBigOTVS_comp (g : E →L[𝕜] F) : (g ∘ f)
 lemma _root_.ContinuousLinearMap.isBigOTVS_fun_comp (g : E →L[𝕜] F) : (g <| f ·) =O[𝕜; l] f :=
   g.isBigOTVS_comp
 
+lemma _root_.LinearMap.isBigOTVS_rev_comp (g : E →ₗ[𝕜] F) (hg : comap g (𝓝 0) ≤ 𝓝 0) :
+    f =O[𝕜; l] (g ∘ f) := by
+  constructor
+  intro U hU
+  rcases mem_comap.1 (hg hU) with ⟨V, hV, hgV⟩
+  use V, hV
+  filter_upwards with a
+  refine le_egauge_of_forall_ne_zero (mem_of_mem_nhds hV) fun c hc₀ hc ↦ ?_
+  apply egauge_le_of_mem_smul
+  grw [← hgV, ← (IsUnit.mk0 _ hc₀).preimage_smul_set]
+  exact hc
+
 @[simp]
 lemma IsLittleOTVS.zero (g : α → F) (l : Filter α) : (0 : α → E) =o[𝕜; l] g := by
   refine ⟨fun U hU ↦ ?_⟩

Mathlib/Analysis/Calculus/FDeriv/ContinuousAlternatingMap.lean

@@ -0,0 +1,250 @@
+/-
+Copyright (c) 2025 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+module
+
+public import Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
+public import Mathlib.Analysis.Normed.Module.Alternating.Basic
+
+/-!
+# Derivatives of operations on continuous alternating maps
+
+In this file we prove formulas for the derivatives of
+
+- `ContinuousAlternatingMap.compContinuousLinearMap`, the pullback of a continuous alternating map
+  along a continuous linear map;
+- application of a `ContinuousAlternatingMap` as a function of both the map and the vectors.
+-/
+
+@[expose] public section
+
+variable {𝕜 ι E F G H : Type*}
+  [NontriviallyNormedField 𝕜]
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H]
+
+open ContinuousAlternatingMap
+open scoped Topology BigOperators
+
+section CompContinuousLinearMap
+
+variable
+  {f : E → G [⋀^ι]→L[𝕜] H} {f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
+  {g : E → F →L[𝕜] G} {g' : E →L[𝕜] F →L[𝕜] G}
+  {s : Set E} {x : E}
+
+/-!
+### Derivative of the pullback
+
+In this section we prove a formula for the derivative
+of the pullback of a continuous alternating map along a continuous linear map,
+as a function of both maps.
+-/
+
+theorem ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff [Finite ι] :
+    HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘L f') x ↔
+      HasStrictFDerivAt f f' x := by
+  cases nonempty_fintype ι
+  constructor <;> intro h
+  · rw [hasStrictFDerivAt_iff_isLittleOTVS] at h ⊢
+    refine Asymptotics.IsBigOTVS.trans_isLittleOTVS ?_ h
+    simp only [Function.comp_apply, ← toContinuousMultilinearMapCLM_apply 𝕜,
+      ContinuousLinearMap.comp_apply, ← map_sub]
+    apply LinearMap.isBigOTVS_rev_comp
+    simp [isEmbedding_toContinuousMultilinearMap.nhds_eq_comap]
+  · exact (toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt.comp x h
+
+section HasFDerivAt
+
+variable [Fintype ι] [DecidableEq ι]
+
+theorem ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap
+    (fg : (G [⋀^ι]→L[𝕜] H) × (F →L[𝕜] G)) :
+    HasStrictFDerivAt
+      (fun fg : (G [⋀^ι]→L[𝕜] H) × (F →L[𝕜] G) ↦ fg.1.compContinuousLinearMap fg.2)
+      (compContinuousLinearMapCLM fg.2 ∘L .fst _ _ _ +
+        fg.1.fderivCompContinuousLinearMap fg.2 ∘L .snd _ _ _)
+      fg := by
+  rw [← hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff]
+  have H₁ := ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap
+    (fg.1.1, fun _ : ι ↦ fg.2)
+  have H₂ := ((toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt (x := fg.1))
+  have H₃ := hasStrictFDerivAt_pi.mpr fun i : ι ↦ hasStrictFDerivAt_id (𝕜 := 𝕜) fg.2
+  exact H₁.comp fg (H₂.prodMap fg H₃)
+
+theorem HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap
+    (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
+    HasStrictFDerivAt (fun x ↦ (f x).compContinuousLinearMap (g x))
+      (compContinuousLinearMapCLM (g x) ∘L f' +
+        (f x).fderivCompContinuousLinearMap (g x) ∘L g') x :=
+  hasStrictFDerivAt_compContinuousLinearMap (f x, g x) |>.comp x (hf.prodMk hg)
+
+theorem HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap
+    (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
+    HasFDerivAt (fun x ↦ (f x).compContinuousLinearMap (g x))
+      (compContinuousLinearMapCLM (g x) ∘L f' +
+        (f x).fderivCompContinuousLinearMap (g x) ∘L g') x := by
+  convert hasStrictFDerivAt_compContinuousLinearMap (f x, (g x)) |>.hasFDerivAt
+    |>.comp x (hf.prodMk hg)
+
+theorem HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap
+    (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
+    HasFDerivWithinAt (fun x ↦ (f x).compContinuousLinearMap (g x))
+      (compContinuousLinearMapCLM (g x) ∘L f' +
+        (f x).fderivCompContinuousLinearMap (g x) ∘L g') s x := by
+  convert hasStrictFDerivAt_compContinuousLinearMap (f x, (g x)) |>.hasFDerivAt
+    |>.comp_hasFDerivWithinAt x (hf.prodMk hg)
+
+theorem fderivWithin_continuousAlternatingMapCompContinuousLinearMap
+    (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x)
+    (hs : UniqueDiffWithinAt 𝕜 s x) :
+    fderivWithin 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) s x =
+      compContinuousLinearMapCLM (g x) ∘L fderivWithin 𝕜 f s x +
+        (f x).fderivCompContinuousLinearMap (g x) ∘L fderivWithin 𝕜 g s x :=
+  hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap (hg.hasFDerivWithinAt)
+    |>.fderivWithin hs
+
+theorem fderiv_continuousAlternatingMapCompContinuousLinearMap
+    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
+    fderiv 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) x =
+      compContinuousLinearMapCLM (g x) ∘L fderiv 𝕜 f x +
+        (f x).fderivCompContinuousLinearMap (g x) ∘L fderiv 𝕜 g x :=
+  hf.hasFDerivAt.continuousAlternatingMapCompContinuousLinearMap (hg.hasFDerivAt) |>.fderiv
+
+end HasFDerivAt
+
+/-!
+### Differentiability of the pullback
+
+In this section we prove that the pullback of a continuous alternating map
+along a continuous linear map is differentiable with respect to a parameter,
+provided that both maps are differentiable.
+-/
+
+variable [Finite ι]
+
+theorem DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap
+    (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
+    DifferentiableWithinAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) s x := by
+  cases nonempty_fintype ι
+  classical
+  exact hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivWithinAt
+    |>.differentiableWithinAt
+
+theorem DifferentiableAt.continuousAlternatingMapCompContinuousLinearMap
+    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
+    DifferentiableAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) x := by
+  cases nonempty_fintype ι
+  classical
+  exact hf.hasFDerivAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivAt
+    |>.differentiableAt
+
+end CompContinuousLinearMap
+
+/-!
+### Derivative of a continuous alternating map applied to a tuple of vectors
+
+In this section we prove the formula for the derivative `D_xf(x; g_0(x), ..., g_n(x))`.
+-/
+
+section Apply
+
+variable {f : E → F [⋀^ι]→L[𝕜] G} {f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G}
+  {g : ι → E → F} {g' : ι → E →L[𝕜] F}
+  {s : Set E} {x : E}
+
+section HasFDerivAt
+
+variable [Fintype ι] [DecidableEq ι]
+
+namespace ContinuousAlternatingMap
+
+theorem hasStrictFDerivAt (f : E [⋀^ι]→L[𝕜] F) (x : ι → E) :
+    HasStrictFDerivAt f (f.1.linearDeriv x) x :=
+  f.1.hasStrictFDerivAt x
+
+theorem hasFDerivAt (f : E [⋀^ι]→L[𝕜] F) (x : ι → E) : HasFDerivAt f (f.1.linearDeriv x) x :=
+  f.1.hasFDerivAt x
+
+theorem hasFDerivWithinAt (f : E [⋀^ι]→L[𝕜] F) (s : Set (ι → E)) (x : ι → E) :
+    HasFDerivWithinAt f (f.1.linearDeriv x) s x :=
+  (f.hasFDerivAt x).hasFDerivWithinAt
+
+end ContinuousAlternatingMap
+
+theorem HasStrictFDerivAt.continuousAlternatingMap_apply (hf : HasStrictFDerivAt f f' x)
+    (hg : ∀ i, HasStrictFDerivAt (g i) (g' i) x) :
+    HasStrictFDerivAt
+      (fun x ↦ f x (g · x))
+      (apply 𝕜 F G (g · x) ∘L f' + ∑ i, (f x).toContinuousLinearMap (g · x) i ∘L g' i)
+      x :=
+  (toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt.comp x hf
+    |>.continuousMultilinearMap_apply hg
+
+theorem HasFDerivAt.continuousAlternatingMap_apply (hf : HasFDerivAt f f' x)
+    (hg : ∀ i, HasFDerivAt (g i) (g' i) x) :
+    HasFDerivAt
+      (fun x ↦ f x (g · x))
+      (apply 𝕜 F G (g · x) ∘L f' + ∑ i, (f x).toContinuousLinearMap (g · x) i ∘L g' i)
+      x :=
+  (toContinuousMultilinearMapCLM 𝕜).hasFDerivAt.comp x hf
+    |>.continuousMultilinearMap_apply hg
+
+theorem HasFDerivWithinAt.continuousAlternatingMap_apply (hf : HasFDerivWithinAt f f' s x)
+    (hg : ∀ i, HasFDerivWithinAt (g i) (g' i) s x) :
+    HasFDerivWithinAt
+      (fun x ↦ f x (g · x))
+      (apply 𝕜 F G (g · x) ∘L f' + ∑ i, (f x).toContinuousLinearMap (g · x) i ∘L g' i)
+      s x :=
+  (toContinuousMultilinearMapCLM 𝕜).hasFDerivAt.comp_hasFDerivWithinAt x hf
+    |>.continuousMultilinearMap_apply hg
+
+theorem fderivWithin_continuousAlternatingMap_apply (hf : DifferentiableWithinAt 𝕜 f s x)
+    (hg : ∀ i, DifferentiableWithinAt 𝕜 (g i) s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
+    fderivWithin 𝕜 (fun x ↦ f x (g · x)) s x =
+      apply 𝕜 F G (g · x) ∘L fderivWithin 𝕜 f s x +
+        ∑ i, (f x).toContinuousLinearMap (g · x) i ∘L fderivWithin 𝕜 (g i) s x :=
+  hf.hasFDerivWithinAt.continuousAlternatingMap_apply (fun i ↦ (hg i).hasFDerivWithinAt)
+    |>.fderivWithin hs
+
+theorem fderiv_continuousAlternatingMap_apply (hf : DifferentiableAt 𝕜 f x)
+    (hg : ∀ i, DifferentiableAt 𝕜 (g i) x) :
+    fderiv 𝕜 (fun x ↦ f x (g · x)) x =
+      apply 𝕜 F G (g · x) ∘L fderiv 𝕜 f x +
+        ∑ i, (f x).toContinuousLinearMap (g · x) i ∘L fderiv 𝕜 (g i) x :=
+  hf.hasFDerivAt.continuousAlternatingMap_apply (fun i ↦ (hg i).hasFDerivAt) |>.fderiv
+
+end HasFDerivAt
+
+variable [Finite ι]
+
+theorem DifferentiableWithinAt.continuousAlternatingMap_apply (hf : DifferentiableWithinAt 𝕜 f s x)
+    (hg : ∀ i, DifferentiableWithinAt 𝕜 (g i) s x) :
+    DifferentiableWithinAt 𝕜 (fun x ↦ f x (g · x)) s x := by
+  cases nonempty_fintype ι
+  classical
+  exact hf.hasFDerivWithinAt.continuousAlternatingMap_apply (fun i ↦ (hg i).hasFDerivWithinAt)
+    |>.differentiableWithinAt
+
+theorem DifferentiableAt.continuousAlternatingMap_apply (hf : DifferentiableAt 𝕜 f x)
+    (hg : ∀ i, DifferentiableAt 𝕜 (g i) x) : DifferentiableAt 𝕜 (fun x ↦ f x (g · x)) x := by
+  cases nonempty_fintype ι
+  classical
+  exact hf.hasFDerivAt.continuousAlternatingMap_apply (fun i ↦ (hg i).hasFDerivAt)
+    |>.differentiableAt
+
+theorem DifferentiableOn.continuousAlternatingMap_apply (hf : DifferentiableOn 𝕜 f s)
+    (hg : ∀ i, DifferentiableOn 𝕜 (g i) s) : DifferentiableOn 𝕜 (fun x ↦ f x (g · x)) s :=
+  fun x hx ↦ (hf x hx).continuousAlternatingMap_apply (hg · x hx)
+
+theorem Differentiable.continuousAlternatingMap_apply (hf : Differentiable 𝕜 f)
+    (hg : ∀ i, Differentiable 𝕜 (g i)) : Differentiable 𝕜 (fun x ↦ f x (g · x)) :=
+  fun x ↦ (hf x).continuousAlternatingMap_apply (hg · x)
+
+theorem ContinuousAlternatingMap.differentiable (f : E [⋀^ι]→L[𝕜] F) : Differentiable 𝕜 f := by
+  cases nonempty_fintype ι
+  apply Differentiable.continuousAlternatingMap_apply <;> fun_prop
+
+end Apply