Merge branch 'master' into D-Thomine/null_measurable_things

Author: D-Thomine

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 57c68e7faac5aea96e58a94ca4a334a1999f0d31
+    default: 7b1f509a52f9a9b56cbe46eb06885aef458fd5bb
   path:
     description: Checkout destination path.
     required: false

Mathlib.lean

@@ -2113,6 +2113,7 @@ public import Mathlib.Analysis.LocallyConvex.WithSeminorms
 public import Mathlib.Analysis.Matrix.Hermitian
 public import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
 public import Mathlib.Analysis.Matrix.LDL
+public import Mathlib.Analysis.Matrix.MeasurableSpace
 public import Mathlib.Analysis.Matrix.Normed
 public import Mathlib.Analysis.Matrix.Order
 public import Mathlib.Analysis.Matrix.PosDef
@@ -2361,6 +2362,7 @@ public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpo
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
+public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Measurable
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
 public import Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
@@ -7650,6 +7652,7 @@ public import Mathlib.Topology.Algebra.Constructions
 public import Mathlib.Topology.Algebra.Constructions.DomMulAct
 public import Mathlib.Topology.Algebra.ContinuousAffineEquiv
 public import Mathlib.Topology.Algebra.ContinuousAffineMap
+public import Mathlib.Topology.Algebra.ContinuousAffineMap.Topology
 public import Mathlib.Topology.Algebra.ContinuousMonoidHom
 public import Mathlib.Topology.Algebra.Equicontinuity
 public import Mathlib.Topology.Algebra.Field
@@ -7711,6 +7714,7 @@ public import Mathlib.Topology.Algebra.Module.ClosedSubmodule
 public import Mathlib.Topology.Algebra.Module.Compact
 public import Mathlib.Topology.Algebra.Module.Complement
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
+public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Extend
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

@@ -16,7 +16,7 @@ This file contains theorems relevant to big operators over `Finset.NatAntidiagon
 
 public section
 
-variable {M N : Type*} [CommMonoid M] [AddCommMonoid N]
+variable {M : Type*} [CommMonoid M]
 
 namespace Finset
 

Mathlib/Algebra/Group/Subgroup/Actions.lean

@@ -27,6 +27,10 @@ variable {G α β : Type*} [Group G]
 section MulAction
 variable [MulAction G α] {S : Subgroup G}
 
+/-- This shortcut instance provides a speedup. -/
+@[to_additive /-- This shortcut instance provides a speedup. -/]
+instance : MulAction S α := inferInstance
+
 @[to_additive] lemma smul_def (g : S) (m : α) : g • m = (g : G) • m := rfl
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -158,6 +158,10 @@ theorem card_le_card_group [Finite G] : Nat.card H ≤ Nat.card G :=
 theorem card_le_of_le {H K : Subgroup G} [Finite K] (h : H ≤ K) : Nat.card H ≤ Nat.card K :=
   Nat.card_le_card_of_injective _ (Subgroup.inclusion_injective h)
 
+@[to_additive]
+theorem card_lt_of_lt {H K : Subgroup G} [Finite K] (h : H < K) : Nat.card H < Nat.card K :=
+  (Set.toFinite _).card_lt_card h
+
 @[to_additive]
 theorem card_map_of_injective {H : Type*} [Group H] {K : Subgroup G} {f : G →* H}
     (hf : Function.Injective f) :

Mathlib/Algebra/Polynomial/Roots.lean

@@ -144,6 +144,16 @@ theorem finite_setOfPred_isRoot {p : R[X]} (hp : p ≠ 0) : Set.Finite { x | IsR
 
 @[deprecated (since := "2026-07-09")] alias finite_setOf_isRoot := finite_setOfPred_isRoot
 
+/-- Nonzero polynomials have no roots away from a finite set. -/
+lemma eventually_cofinite_not_isRoot {p : R[X]} (hp : p ≠ 0) :
+    ∀ᶠ x in Filter.cofinite, ¬p.IsRoot x :=
+  (finite_setOfPred_isRoot hp).compl_mem_cofinite
+
+/-- Nonzero polynomials are nonzero away from a finite set. -/
+lemma eventually_eval_ne_zero_cofinite {p : R[X]} (hp : p ≠ 0) :
+    ∀ᶠ x in Filter.cofinite, p.eval x ≠ 0 :=
+  eventually_cofinite_not_isRoot hp
+
 theorem eq_zero_of_infinite_isRoot (p : R[X]) (h : Set.Infinite { x | IsRoot p x }) : p = 0 :=
   not_imp_comm.mp finite_setOfPred_isRoot h
 

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -658,6 +658,46 @@ theorem Filter.EventuallyEq.nhdsNE_deriv (h : f₁ =ᶠ[𝓝[≠] x] f) : deriv
   filter_upwards [h] with y hy
   apply Filter.EventuallyEq.deriv hy
 
+/--
+If two functions agree on a codiscrete subset of `s`, then so do their derivatives within any
+subset `t` of `s`.
+-/
+theorem Filter.EventuallyEq.codiscreteWithin_derivWithin'
+    (h : f₁ =ᶠ[codiscreteWithin s] f) (ht : t ⊆ s) :
+    derivWithin f₁ t =ᶠ[codiscreteWithin s] derivWithin f t := by
+  filter_upwards [h.codiscreteWithin_fderivWithin' (𝕜 := 𝕜) ht] with y hy
+  simp [derivWithin, hy]
+
+/--
+If two functions agree on a codiscrete subset of `s`, then so do their derivatives within `s`.
+-/
+theorem Filter.EventuallyEq.codiscreteWithin_derivWithin
+    (h : f₁ =ᶠ[codiscreteWithin s] f) :
+    derivWithin f₁ s =ᶠ[codiscreteWithin s] derivWithin f s :=
+  h.codiscreteWithin_derivWithin' Subset.rfl
+
+/--
+If two functions agree on a codiscrete subset of an open set `s`, then so do their derivatives.
+-/
+theorem Filter.EventuallyEq.codiscreteWithin_deriv (h : f₁ =ᶠ[codiscreteWithin s] f)
+    (hs : IsOpen s) :
+    deriv f₁ =ᶠ[codiscreteWithin s] deriv f := by
+  filter_upwards [h.codiscreteWithin_fderiv (𝕜 := 𝕜) hs] with y hy
+  simp_rw [deriv, hy]
+
+/-- If two functions agree on a codiscrete subset of `𝕜`, then so do their derivatives within
+any subset `s` of `𝕜`. -/
+theorem Filter.EventuallyEq.codiscrete_derivWithin
+    (h : f₁ =ᶠ[codiscrete 𝕜] f) :
+    derivWithin f₁ s =ᶠ[codiscrete 𝕜] derivWithin f s :=
+  h.codiscreteWithin_derivWithin' <| subset_univ _
+
+/-- If two functions agree on a codiscrete subset of `𝕜`, then so do their derivatives. -/
+theorem Filter.EventuallyEq.codiscrete_deriv
+    (h : f₁ =ᶠ[codiscrete 𝕜] f) :
+    deriv f₁ =ᶠ[codiscrete 𝕜] deriv f :=
+  h.codiscreteWithin_deriv isOpen_univ
+
 end congr
 
 section id

Mathlib/Analysis/Calculus/FDeriv/Congr.lean

@@ -261,6 +261,47 @@ theorem Filter.EventuallyEq.fderiv_eq (h : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f
 protected theorem Filter.EventuallyEq.fderiv (h : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ =ᶠ[𝓝 x] fderiv 𝕜 f :=
   h.eventuallyEq_nhds.mono fun _ h => h.fderiv_eq
 
+/-- If two functions agree on a codiscrete subset of `s`, then so do their derivatives within
+any subset `t` of `s`. -/
+theorem Filter.EventuallyEq.codiscreteWithin_fderivWithin'
+    (h : f₁ =ᶠ[codiscreteWithin s] f) (ht : t ⊆ s) :
+    fderivWithin 𝕜 f₁ t =ᶠ[codiscreteWithin s] fderivWithin 𝕜 f t := by
+  filter_upwards [h, self_mem_codiscreteWithin s] with x hx hxs
+  have hsx : f₁ =ᶠ[𝓝[s] x] f := by
+    rw [← insert_sdiff_self_of_mem hxs, nhdsWithin_insert, EventuallyEq,
+      eventually_sup, eventually_pure]
+    exact ⟨hx, eventuallyEq_codiscreteWithin_iff_forall_eventuallyEq_nhdsWithin.1 h x hxs⟩
+  exact (hsx.filter_mono <| nhdsWithin_mono x ht).fderivWithin_eq hx
+
+/-- If two functions agree on a codiscrete subset of `s`, then so do their derivatives
+within `s`. -/
+theorem Filter.EventuallyEq.codiscreteWithin_fderivWithin
+    (h : f₁ =ᶠ[codiscreteWithin s] f) :
+    fderivWithin 𝕜 f₁ s =ᶠ[codiscreteWithin s] fderivWithin 𝕜 f s :=
+  h.codiscreteWithin_fderivWithin' Subset.rfl
+
+/-- If two functions agree on a codiscrete subset of an open set `s`, then so do their
+derivatives. -/
+theorem Filter.EventuallyEq.codiscreteWithin_fderiv
+    (h : f₁ =ᶠ[codiscreteWithin s] f) (hs : IsOpen s) :
+    fderiv 𝕜 f₁ =ᶠ[codiscreteWithin s] fderiv 𝕜 f := by
+  filter_upwards [h.codiscreteWithin_fderivWithin (𝕜 := 𝕜), self_mem_codiscreteWithin s]
+  intro x hx hxs
+  simp_all [fderivWithin_of_isOpen]
+
+/-- If two functions agree on a codiscrete subset of `E`, then so do their derivatives within
+any subset `s` of `E`. -/
+theorem Filter.EventuallyEq.codiscrete_fderivWithin
+    (h : f₁ =ᶠ[codiscrete E] f) :
+    fderivWithin 𝕜 f₁ s =ᶠ[codiscrete E] fderivWithin 𝕜 f s :=
+  h.codiscreteWithin_fderivWithin' <| subset_univ _
+
+/-- If two functions agree on a codiscrete subset of `E`, then so do their derivatives. -/
+theorem Filter.EventuallyEq.codiscrete_fderiv
+    (h : f₁ =ᶠ[codiscrete E] f) :
+    fderiv 𝕜 f₁ =ᶠ[codiscrete E] fderiv 𝕜 f :=
+  h.codiscreteWithin_fderiv isOpen_univ
+
 end congr
 
 end

Mathlib/Analysis/Complex/JensenFormula.lean

@@ -368,7 +368,7 @@ theorem MeromorphicOn.circleAverage_log_norm {c : ℂ} {R : ℝ} {f : ℂ → 
     rw [circleAverage_congr_codiscreteWithin (f₂ := 0) _ hR]
     · simp only [circleAverage, mul_inv_rev, Pi.zero_apply, intervalIntegral.integral_zero,
         smul_eq_mul, mul_zero]
-    apply Filter.codiscreteWithin_mono (U := CB) sphere_subset_closedBall
+    apply Filter.codiscreteWithin_mono (s := CB) sphere_subset_closedBall
     filter_upwards [this] with z hz
     simp_all
 

Mathlib/Analysis/Distribution/TemperateGrowth.lean

@@ -302,15 +302,6 @@ lemma _root_.ContinuousLinearEquiv.hasTemperateGrowth (f : E ≃L[ℝ] F) :
     Function.HasTemperateGrowth f :=
   f.toContinuousLinearMap.hasTemperateGrowth
 
-@[fun_prop]
-theorem Complex.hasTemperateGrowth_ofReal : Complex.ofReal.HasTemperateGrowth :=
-  (Complex.ofRealCLM).hasTemperateGrowth
-
-variable (𝕜) in
-@[fun_prop]
-theorem RCLike.hasTemperateGrowth_ofReal [RCLike 𝕜] : (RCLike.ofReal (K := 𝕜)).HasTemperateGrowth :=
-  (RCLike.ofRealCLM (K := 𝕜)).hasTemperateGrowth
-
 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H]
 
 @[fun_prop]
@@ -412,6 +403,72 @@ theorem hasTemperateGrowth_one_add_norm_sq_rpow (r : ℝ) :
 
 end Function
 
+section Real
+
+@[fun_prop]
+theorem Real.hasTemperateGrowth_sin :
+    Real.sin.HasTemperateGrowth := by
+  refine ⟨Real.contDiff_sin, fun n ↦ ⟨0, 1, fun x ↦ ?_⟩⟩
+  simpa [norm_iteratedFDeriv_eq_norm_iteratedDeriv] using Real.abs_iteratedDeriv_sin_le_one n x
+
+@[fun_prop]
+theorem Real.hasTemperateGrowth_cos :
+    Real.cos.HasTemperateGrowth := by
+  refine ⟨Real.contDiff_cos, fun n ↦ ⟨0, 1, fun x ↦ ?_⟩⟩
+  simpa [norm_iteratedFDeriv_eq_norm_iteratedDeriv] using Real.abs_iteratedDeriv_cos_le_one n x
+
+end Real
+
+section Complex
+
+@[fun_prop]
+theorem Complex.hasTemperateGrowth_ofReal : Complex.ofReal.HasTemperateGrowth :=
+  Complex.ofRealCLM.hasTemperateGrowth
+
+@[deprecated (since := "2026-08-18")] alias Function.Complex.hasTemperateGrowth_ofReal :=
+  Complex.hasTemperateGrowth_ofReal
+
+@[fun_prop]
+theorem Complex.hasTemperateGrowth_re : Complex.re.HasTemperateGrowth :=
+  Complex.reCLM.hasTemperateGrowth
+
+@[fun_prop]
+theorem Complex.hasTemperateGrowth_im : Complex.im.HasTemperateGrowth :=
+  Complex.imCLM.hasTemperateGrowth
+
+/-- The function `x ↦ exp (x * I)` has temperate growth. -/
+@[fun_prop]
+theorem Complex.hasTemperateGrowth_exp_mul_I :
+    (fun x : ℝ ↦ Complex.exp (x * Complex.I)).HasTemperateGrowth := by
+  simp only [Complex.exp_ofReal_mul_I]
+  fun_prop
+
+end Complex
+
+section RCLike
+
+variable [RCLike 𝕜]
+
+variable (𝕜) in
+@[fun_prop]
+theorem RCLike.hasTemperateGrowth_ofReal : (RCLike.ofReal (K := 𝕜)).HasTemperateGrowth :=
+  (RCLike.ofRealCLM (K := 𝕜)).hasTemperateGrowth
+
+@[deprecated (since := "2026-08-18")] alias Function.RCLike.hasTemperateGrowth_ofReal :=
+  RCLike.hasTemperateGrowth_ofReal
+
+variable (𝕜) in
+@[fun_prop]
+theorem RCLike.hasTemperateGrowth_re : (RCLike.re : 𝕜 → ℝ).HasTemperateGrowth :=
+  (RCLike.reCLM (K := 𝕜)).hasTemperateGrowth
+
+variable (𝕜) in
+@[fun_prop]
+theorem RCLike.hasTemperateGrowth_im : (RCLike.im : 𝕜 → ℝ).HasTemperateGrowth :=
+  (RCLike.imCLM (K := 𝕜)).hasTemperateGrowth
+
+end RCLike
+
 namespace MeasureTheory.Measure
 
 variable [NormedAddCommGroup E] [MeasurableSpace E]