feat(Geometry/Manifold): continuously differentiable actions

Mathlib.lean

@@ -1855,6 +1855,7 @@ public import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
 public import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
 public import Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
 public import Mathlib.Analysis.ConstantSpeed
+public import Mathlib.Analysis.ContDiffMulAction
 public import Mathlib.Analysis.Convex.AmpleSet
 public import Mathlib.Analysis.Convex.Approximation
 public import Mathlib.Analysis.Convex.Basic

Mathlib/Analysis/ContDiffMulAction.lean

@@ -0,0 +1,280 @@
+/-
+Copyright (c) 2026 Archibald Browne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Archibald Browne
+-/
+module
+
+
+public import Mathlib.Analysis.Calculus.ContDiff.Operations
+
+/-!
+# Continuously differentiable monoid actions
+
+In this file we define the class `ContDiffSMul`. `ContDiffSMul 𝕜 M X n` holds if `M` acts on `X` and
+the map `(c, x) ↦ c • x` is `n` times continuously differentiable on `M × X`.
+
+## Main definitions
+
+* `ContDiffSMul 𝕜 M X n` : typeclass saying that the map `(c, x) ↦ c • x` is `n` times continuously
+  differentiable on `M × X`
+
+## Main results
+
+`ContDiffSMul.of_retraction`, `ContinuousLinearEquiv.contDiffSMul` and `ContDiffSMul.comp` prove
+results about pullbacks of continuously differentiable actions. `ContDiff.contdiff_smul`
+provides dot-syntax for `ContDiffSMul`. Many of the results here are the continuously differentiable
+analogues of the results in the module `Mathlib.Topology.Algebra.MulAction`.
+-/
+
+@[expose] public section
+
+open Topology Pointwise
+open Filter
+
+
+/-- The class `ContDiffVAdd 𝕜 M X n` says that the additive action `(+ᵥ) : M → X → X`
+is `n` times continuously differentiable on `M × X`. -/
+class ContDiffVAdd (𝕜 M X : Type*) (n : WithTop ℕ∞) [VAdd M X] [NormedAddCommGroup X]
+    [NontriviallyNormedField 𝕜] [NormedAddCommGroup M] [NormedSpace 𝕜 M]
+    [NormedSpace 𝕜 X] : Prop where
+  /-- The additive action `(+ᵥ)` is continuous. -/
+  contdiff_vadd : ContDiff 𝕜 n fun p : M × X => p.1 +ᵥ p.2
+
+
+
+/-- The class `ContDiffSMul 𝕜 M X n` says that the scalar multiplication `(•) : M → X → X` is `n`
+times continuously differentiable on `M × X`. -/
+@[to_additive]
+class ContDiffSMul (𝕜 M X : Type*) (n : WithTop ℕ∞) [SMul M X] [NormedAddCommGroup X]
+    [NontriviallyNormedField 𝕜] [NormedAddCommGroup M] [NormedSpace 𝕜 M]
+    [NormedSpace 𝕜 X] : Prop where
+  /-- The scalar multiplication `(•)` is continuously differentiable. -/
+  contdiff_smul : ContDiff 𝕜 n fun p : M × X => p.1 • p.2
+
+export ContDiffSMul (contdiff_smul)
+
+
+
+export ContDiffVAdd (contdiff_vadd)
+
+
+attribute [continuity, fun_prop] contdiff_smul contdiff_vadd
+
+@[to_additive]
+-- Cannot be an instance: `𝕜` and `n` don't appear in the conclusion
+theorem ContDiffSMul.toContinuousSMul (𝕜 : Type*) {M X : Type*} (n : WithTop ℕ∞)
+    [NontriviallyNormedField 𝕜] [SMul M X]
+    [NormedAddCommGroup M] [NormedSpace 𝕜 M]
+    [NormedAddCommGroup X] [NormedSpace 𝕜 X]
+    [ContDiffSMul 𝕜 M X n] : ContinuousSMul M X where
+  continuous_smul := (contdiff_smul (𝕜 := 𝕜) (n := n)).continuous
+
+section Main
+
+variable {𝕜 M X Y α : Type*} {n : WithTop ℕ∞} [NontriviallyNormedField 𝕜]
+  [NormedAddCommGroup M] [NormedSpace 𝕜 M]
+  [NormedAddCommGroup X] [NormedSpace 𝕜 X]
+
+theorem ContDiffSMul.of_le {m : WithTop ℕ∞} [SMul M X] [ContDiffSMul 𝕜 M X n] (h : m ≤ n) :
+    ContDiffSMul 𝕜 M X m where
+  contdiff_smul := contdiff_smul.of_le h
+
+
+section SMul
+
+variable [SMul M X] [ContDiffSMul 𝕜 M X n]
+
+@[to_additive]
+lemma IsScalarTower.contdiffSMul {M : Type*} (N : Type*) {α : Type*} [Monoid N] [SMul M N]
+    [MulAction N α] [SMul M α] [IsScalarTower M N α]
+    [NormedAddCommGroup α] [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace 𝕜 M]
+    [NormedSpace 𝕜 N] [NormedSpace 𝕜 α] [ContDiffSMul 𝕜 M N n]
+    [ContDiffSMul 𝕜 N α n] : ContDiffSMul 𝕜 M α n where
+  contdiff_smul := by
+    suffices ContDiff 𝕜 n (fun p : M × α ↦ (p.1 • (1 : N)) • p.2) by
+      simpa [smul_one_smul N]
+    have h1 : ContDiff 𝕜 n (fun p : M × α ↦ p.1 • (1 : N)) :=
+      (ContDiffSMul.contdiff_smul (𝕜 := 𝕜) (M := M) (X := N) (n := n)).comp
+        (ContDiff.prodMk contDiff_fst contDiff_const)
+    exact (ContDiffSMul.contdiff_smul (𝕜 := 𝕜) (M := N) (X := α) (n := n)).comp
+      (ContDiff.prodMk h1 contDiff_snd)
+
+@[to_additive]
+lemma MulOpposite.contDiff_op : ContDiff 𝕜 n (op : M → Mᵐᵒᵖ) :=
+  (MulOpposite.opContinuousLinearEquiv 𝕜 : M ≃L[𝕜] Mᵐᵒᵖ).contDiff
+
+lemma MulOpposite.contDiff_unop : ContDiff 𝕜 n (unop : Mᵐᵒᵖ → M) :=
+  (MulOpposite.opContinuousLinearEquiv 𝕜 : M ≃L[𝕜] Mᵐᵒᵖ).symm.contDiff
+
+@[to_additive]
+instance ContDiffSMul.op [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : ContDiffSMul 𝕜 Mᵐᵒᵖ X n :=
+  ⟨by
+    suffices ContDiff 𝕜 n fun p : M × X => MulOpposite.op p.fst • p.snd from
+      this.comp ((MulOpposite.contDiff_unop (n := n)).prodMap contDiff_id)
+    simpa only [op_smul_eq_smul] using (contdiff_smul : ContDiff 𝕜 n fun p : M × X => _)⟩
+
+@[to_additive]
+instance MulOpposite.contDiffSMul : ContDiffSMul 𝕜 M Xᵐᵒᵖ n :=
+  ⟨(MulOpposite.contDiff_op (n := n)).comp <|
+    contdiff_smul.comp <| contDiff_id.prodMap (MulOpposite.contDiff_unop (n := n))⟩
+
+section Transfer
+
+variable {N Y : Type*} [NormedAddCommGroup N] [NormedSpace 𝕜 N]
+  [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
+
+
+/-- Transfer `ContDiffSMul` along a `ContinuousLinearEquiv`.
+Analogue of `Topology.IsInducing.continuousSMul` for the smooth setting. -/
+@[to_additive]
+lemma ContinuousLinearEquiv.contDiffSMul [SMul N Y] {f : N → M}
+    (g : Y ≃L[𝕜] X) (hf : ContDiff 𝕜 n f)
+    (hsmul : ∀ {c y}, g (c • y) = f c • g y) :
+    ContDiffSMul 𝕜 N Y n := ⟨by
+  set F := fun (p : N × Y) => p.1 • p.2 with hF
+  have hF' : F = (fun p ↦ g.symm (g (p.1 • p.2))) := by
+    ext p; simp only [symm_apply_apply, hF]
+  simp_rw [hsmul] at hF'
+  rw [hF']
+  exact g.symm.contDiff.comp
+    (contdiff_smul.comp (ContDiff.prodMk (hf.comp contDiff_fst)
+      (g.contDiff.comp contDiff_snd)))⟩
+
+/-- Transfer `ContDiffSMul` via a retraction (continuous linear left inverse).
+Analogue of `SMulMemClass.continuousSMul` for complemented subspaces. -/
+@[to_additive]
+lemma ContDiffSMul.of_retraction [SMul M N]
+    (ι : N →L[𝕜] X) (π : X →L[𝕜] N) (hπι : ∀ x, π (ι x) = x)
+    (hsmul : ∀ (m : M) (x : N), ι (m • x) = m • ι x) : ContDiffSMul 𝕜 M N n := ⟨by
+  set F := fun (p : M × N) => p.1 • p.2 with hF
+  have hF' : F = fun p ↦ π (p.1 • ι p.2) := by
+    ext p; rw [← hsmul p.1 p.2, hπι (p.1 • p.2)]
+  rw [hF']
+  exact π.contDiff.comp (contdiff_smul.comp
+    (ContDiff.prodMk contDiff_fst (ι.contDiff.comp contDiff_snd)))⟩
+
+/-- Transfer `ContDiffSMul` along a continuously differentiable map on the acting type. -/
+@[to_additive]
+lemma ContDiffSMul.comp [SMul N X] {f : N → M}
+    (hf : ContDiff 𝕜 n f)
+    (hsmul : ∀ (c : N) (x : X), c • x = f c • x) :
+    ContDiffSMul 𝕜 N X n := ⟨by
+  set F := fun p : N × X => p.1 • p.2 with hF
+  have : F = fun p => f p.1 • p.2 := by
+    ext p; rw [← hsmul p.1 p.2]
+  simpa [this] using
+    contdiff_smul.comp (ContDiff.prodMk (hf.comp contDiff_fst) contDiff_snd)⟩
+
+end Transfer
+
+variable {f : Y → M} {g : Y → X} {b : Y} {s : Set Y} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
+
+@[to_additive]
+theorem ContDiffWithinAt.contdiff_smul'
+    (hf : ContDiffWithinAt 𝕜 n f s b) (hg : ContDiffWithinAt 𝕜 n g s b) :
+    ContDiffWithinAt 𝕜 n (fun x => f x • g x) s b :=
+  ContDiffSMul.contdiff_smul.comp_contDiffWithinAt (ContDiffWithinAt.prodMk hf hg)
+
+@[to_additive]
+theorem ContDiffAt.contdiff_smul (hf : ContDiffAt 𝕜 n f b)
+    (hg : ContDiffAt 𝕜 n g b) :
+    ContDiffAt 𝕜 n (fun x => f x • g x) b :=
+  ContDiffSMul.contdiff_smul.comp_contDiffAt _ (ContDiffAt.prodMk hf hg)
+
+@[to_additive]
+theorem ContDiffOn.contdiff_smul (hf : ContDiffOn 𝕜 n f s)
+    (hg : ContDiffOn 𝕜 n g s) :
+    ContDiffOn 𝕜 n (fun x => f x • g x) s :=
+  fun x hx => (hf x hx).contdiff_smul' (hg x hx)
+
+@[to_additive]
+theorem ContDiff.contdiff_smul (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
+    ContDiff 𝕜 n (fun x => f x • g x) :=
+  ContDiffSMul.contdiff_smul.comp (ContDiff.prodMk hf hg)
+
+end SMul
+
+section Monoid
+
+variable [Monoid M] [MulAction M X] [ContDiffSMul 𝕜 M X n]
+
+theorem MulAction.contDiffSMul_compHom {N} [NormedAddCommGroup N] [NormedSpace 𝕜 N]
+    [Monoid N] {f : N →* M} (hf : ContDiff 𝕜 n f) :
+    letI := MulAction.compHom X f
+    ContDiffSMul 𝕜 N X n := by
+  letI := MulAction.compHom X f
+  exact ⟨(hf.comp contDiff_fst).contdiff_smul contDiff_snd⟩
+
+
+end Monoid
+
+section Normed
+
+variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+
+/-- Scalar multiplication by a normed field on a normed space is C^n. -/
+instance NormedSpace.contDiffSMul {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+    [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] :
+    ContDiffSMul 𝕜 𝕜' F n where
+  contdiff_smul := contDiff_smul
+
+
+/-- Multiplication in a normed algebra is C^n as a scalar action on itself. -/
+instance NormedAlgebra.contDiffSMul_self {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] :
+    ContDiffSMul 𝕜 A A n where
+  contdiff_smul := contDiff_mul
+
+end Normed
+
+instance ContinuousLinearMap.contDiffSMul :
+    ContDiffSMul 𝕜 (M →L[𝕜] M) M n where
+  contdiff_smul := isBoundedBilinearMap_apply.contDiff
+
+variable [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
+
+instance Prod.contDiffSMul [SMul M X] [SMul M Y] [ContDiffSMul 𝕜 M X n] [ContDiffSMul 𝕜 M Y n] :
+    ContDiffSMul 𝕜 M (X × Y) n where
+  contdiff_smul := by
+    suffices ContDiff 𝕜 n (fun p : M × (X × Y) => p.1 • p.2) by
+      simpa only [Prod.smul_def] using this
+    refine ContDiff.prodMk ?_ ?_
+    · exact ContDiff.contdiff_smul contDiff_fst (ContDiff.snd' contDiff_fst)
+    · exact ContDiff.contdiff_smul contDiff_fst (ContDiff.snd' contDiff_snd)
+
+instance {ι : Type*} [Fintype ι] {γ : ι → Type*} [∀ i, SMul M (γ i)]
+    [∀ i, NormedAddCommGroup (γ i)]
+    [∀ i, NormedSpace 𝕜 (γ i)] [∀ i, ContDiffSMul 𝕜 M (γ i) n] :
+    ContDiffSMul 𝕜 M (∀ i, γ i) n :=
+  ⟨contDiff_pi.mpr fun i => by
+    simp only [Pi.smul_apply]
+    have hi : ContDiff 𝕜 n (fun x : M × (∀ i, γ i) => x.2 i) :=
+      (ContinuousLinearMap.proj (R := 𝕜) (ι := ι) (φ := γ) i).contDiff.comp contDiff_snd
+    exact contDiff_fst.contdiff_smul hi⟩
+
+end Main
+
+section Tendsto
+
+variable {𝕜 M X α : Type*}
+
+@[to_additive]
+theorem Filter.Tendsto.contdiff_smul (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+    [NormedAddCommGroup M] [NormedSpace 𝕜 M] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
+    [SMul M X] (n : WithTop ℕ∞) [ContDiffSMul 𝕜 M X n]
+    {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X}
+    (hf : Tendsto f l (𝓝 c)) (hg : Tendsto g l (𝓝 a)) :
+    Tendsto (fun x => f x • g x) l (𝓝 <| c • a) :=
+  (ContDiffSMul.contdiff_smul (𝕜 := 𝕜) (n := n) |>.continuous.tendsto _).comp
+    (hf.prodMk_nhds hg)
+
+@[to_additive]
+theorem Filter.Tendsto.contdiff_smul_const (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+    [NormedAddCommGroup M] [NormedSpace 𝕜 M] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
+    [SMul M X] (n : WithTop ℕ∞) [ContDiffSMul 𝕜 M X n]
+    {f : α → M} {l : Filter α} {c : M}
+    (hf : Tendsto f l (𝓝 c)) (a : X) :
+    Tendsto (fun x => f x • a) l (𝓝 (c • a)) :=
+  hf.contdiff_smul 𝕜 n tendsto_const_nhds
+
+end Tendsto