Skip to content

Commit

Permalink
feat: finite products/sums of differentiable maps into smooth commuta…
Browse files Browse the repository at this point in the history 
…tive monoids are differentiable (#9775)

From sphere-eversion; I'm just upstreaming this.



Co-authored-by: Oliver Nash <[email protected]>
  • Loading branch information
@grunweg @ocfnash
grunweg and ocfnash committed Jan 24, 2024
1 parent 0aa016e commit a686ba8
Showing 1 changed file with 113 additions and 65 deletions.
178 changes: 113 additions & 65 deletions Mathlib/Geometry/Manifold/Algebra/Monoid.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -299,16 +299,39 @@ instance : ContinuousMapClass (SmoothMonoidMorphism I I' G G') G G' where

end Monoid

/-! ### Differentiability of finite point-wise sums and products
Finite point-wise products (resp. sums) of differentiable/smooth functions `M → G` (at `x`/on `s`)
into a commutative monoid `G` are differentiable/smooth at `x`/on `s`. -/
section CommMonoid

open Function
open scoped BigOperators

variable {ι 𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [TopologicalSpace H] {E : Type*}
[NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type*} [CommMonoid G]
[TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type*} [NormedAddCommGroup E']
[NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
{M : Type*} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
{f : ι → M → G} {n : ℕ∞} {p : ι → Prop}
variable {ι 𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [TopologicalSpace H]
{E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H}
{G : Type*} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G]
{E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
{H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
{M : Type*} [TopologicalSpace M] [ChartedSpace H' M]
{s : Set M} {x x₀ : M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} {p : ι → Prop}

@[to_additive]
theorem ContMDiffWithinAt.prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) :
ContMDiffWithinAt I' I n (fun x ↦ ∏ i in t, f i x) s x₀ := by
classical
induction' t using Finset.induction_on with i K iK IH
· simp [contMDiffWithinAt_const]
· simp only [iK, Finset.prod_insert, not_false_iff]
exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)

@[to_additive]
theorem contMDiffWithinAt_finprod (lf : LocallyFinite fun i ↦ mulSupport <| f i) {x₀ : M}
(h : ∀ i, ContMDiffWithinAt I' I n (f i) s x₀) :
ContMDiffWithinAt I' I n (fun x ↦ ∏ᶠ i, f i x) s x₀ :=
let ⟨_I, hI⟩ := finprod_eventually_eq_prod lf x₀
(ContMDiffWithinAt.prod fun i _hi ↦ h i).congr_of_eventuallyEq
(eventually_nhdsWithin_of_eventually_nhds hI) hI.self_of_nhds

@[to_additive]
theorem contMDiffWithinAt_finset_prod' (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
Expand All @@ -318,26 +341,6 @@ theorem contMDiffWithinAt_finset_prod' (h : ∀ i ∈ t, ContMDiffWithinAt I' I
#align cont_mdiff_within_at_finset_prod' contMDiffWithinAt_finset_prod'
#align cont_mdiff_within_at_finset_sum' contMDiffWithinAt_finset_sum'

@[to_additive]
theorem contMDiffAt_finset_prod' (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
ContMDiffAt I' I n (∏ i in t, f i) x :=
contMDiffWithinAt_finset_prod' h
#align cont_mdiff_at_finset_prod' contMDiffAt_finset_prod'
#align cont_mdiff_at_finset_sum' contMDiffAt_finset_sum'

@[to_additive]
theorem contMDiffOn_finset_prod' (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
ContMDiffOn I' I n (∏ i in t, f i) s := fun x hx =>
contMDiffWithinAt_finset_prod' fun i hi => h i hi x hx
#align cont_mdiff_on_finset_prod' contMDiffOn_finset_prod'
#align cont_mdiff_on_finset_sum' contMDiffOn_finset_sum'

@[to_additive]
theorem contMDiff_finset_prod' (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
ContMDiff I' I n (∏ i in t, f i) := fun x => contMDiffAt_finset_prod' fun i hi => h i hi x
#align cont_mdiff_finset_prod' contMDiff_finset_prod'
#align cont_mdiff_finset_sum' contMDiff_finset_sum'

@[to_additive]
theorem contMDiffWithinAt_finset_prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
ContMDiffWithinAt I' I n (fun x => ∏ i in t, f i x) s x := by
Expand All @@ -346,20 +349,63 @@ theorem contMDiffWithinAt_finset_prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n
#align cont_mdiff_within_at_finset_prod contMDiffWithinAt_finset_prod
#align cont_mdiff_within_at_finset_sum contMDiffWithinAt_finset_sum

@[to_additive]
theorem ContMDiffAt.prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) :
ContMDiffAt I' I n (fun x ↦ ∏ i in t, f i x) x₀ := by
simp only [← contMDiffWithinAt_univ] at *
exact ContMDiffWithinAt.prod h

@[to_additive]
theorem contMDiffAt_finprod
(lf : LocallyFinite fun i ↦ mulSupport <| f i) (h : ∀ i, ContMDiffAt I' I n (f i) x₀) :
ContMDiffAt I' I n (fun x ↦ ∏ᶠ i, f i x) x₀ :=
contMDiffWithinAt_finprod lf h

@[to_additive]
theorem contMDiffAt_finset_prod' (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
ContMDiffAt I' I n (∏ i in t, f i) x :=
contMDiffWithinAt_finset_prod' h
#align cont_mdiff_at_finset_prod' contMDiffAt_finset_prod'
#align cont_mdiff_at_finset_sum' contMDiffAt_finset_sum'

@[to_additive]
theorem contMDiffAt_finset_prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
ContMDiffAt I' I n (fun x => ∏ i in t, f i x) x :=
contMDiffWithinAt_finset_prod h
#align cont_mdiff_at_finset_prod contMDiffAt_finset_prod
#align cont_mdiff_at_finset_sum contMDiffAt_finset_sum

@[to_additive]
theorem contMDiffOn_finprod
(lf : LocallyFinite fun i ↦ Function.mulSupport <| f i) (h : ∀ i, ContMDiffOn I' I n (f i) s) :
ContMDiffOn I' I n (fun x ↦ ∏ᶠ i, f i x) s := fun x hx ↦
contMDiffWithinAt_finprod lf fun i ↦ h i x hx

@[to_additive]
theorem contMDiffOn_finset_prod' (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
ContMDiffOn I' I n (∏ i in t, f i) s := fun x hx =>
contMDiffWithinAt_finset_prod' fun i hi => h i hi x hx
#align cont_mdiff_on_finset_prod' contMDiffOn_finset_prod'
#align cont_mdiff_on_finset_sum' contMDiffOn_finset_sum'

@[to_additive]
theorem contMDiffOn_finset_prod (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
ContMDiffOn I' I n (fun x => ∏ i in t, f i x) s := fun x hx =>
contMDiffWithinAt_finset_prod fun i hi => h i hi x hx
#align cont_mdiff_on_finset_prod contMDiffOn_finset_prod
#align cont_mdiff_on_finset_sum contMDiffOn_finset_sum

@[to_additive]
theorem ContMDiff.prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
ContMDiff I' I n fun x ↦ ∏ i in t, f i x :=
fun x ↦ ContMDiffAt.prod fun j hj ↦ h j hj x

@[to_additive]
theorem contMDiff_finset_prod' (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
ContMDiff I' I n (∏ i in t, f i) := fun x => contMDiffAt_finset_prod' fun i hi => h i hi x
#align cont_mdiff_finset_prod' contMDiff_finset_prod'
#align cont_mdiff_finset_sum' contMDiff_finset_sum'

@[to_additive]
theorem contMDiff_finset_prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
ContMDiff I' I n fun x => ∏ i in t, f i x := fun x =>
Expand All @@ -368,31 +414,33 @@ theorem contMDiff_finset_prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
#align cont_mdiff_finset_sum contMDiff_finset_sum

@[to_additive]
theorem smoothWithinAt_finset_prod' (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) :
SmoothWithinAt I' I (∏ i in t, f i) s x :=
contMDiffWithinAt_finset_prod' h
#align smooth_within_at_finset_prod' smoothWithinAt_finset_prod'
#align smooth_within_at_finset_sum' smoothWithinAt_finset_sum'
theorem contMDiff_finprod (h : ∀ i, ContMDiff I' I n (f i))
(hfin : LocallyFinite fun i => mulSupport (f i)) : ContMDiff I' I n fun x => ∏ᶠ i, f i x :=
fun x ↦ contMDiffAt_finprod hfin fun i ↦ h i x
#align cont_mdiff_finprod contMDiff_finprod
#align cont_mdiff_finsum contMDiff_finsum

@[to_additive]
theorem smoothAt_finset_prod' (h : ∀ i ∈ t, SmoothAt I' I (f i) x) :
SmoothAt I' I (∏ i in t, f i) x :=
contMDiffAt_finset_prod' h
#align smooth_at_finset_prod' smoothAt_finset_prod'
#align smooth_at_finset_sum' smoothAt_finset_sum'
theorem contMDiff_finprod_cond (hc : ∀ i, p i → ContMDiff I' I n (f i))
(hf : LocallyFinite fun i => mulSupport (f i)) :
ContMDiff I' I n fun x => ∏ᶠ (i) (_ : p i), f i x := by
simp only [← finprod_subtype_eq_finprod_cond]
exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
#align cont_mdiff_finprod_cond contMDiff_finprod_cond
#align cont_mdiff_finsum_cond contMDiff_finsum_cond

@[to_additive]
theorem smoothOn_finset_prod' (h : ∀ i ∈ t, SmoothOn I' I (f i) s) :
SmoothOn I' I (∏ i in t, f i) s :=
contMDiffOn_finset_prod' h
#align smooth_on_finset_prod' smoothOn_finset_prod'
#align smooth_on_finset_sum' smoothOn_finset_sum'
theorem smoothAt_finprod
(lf : LocallyFinite fun i ↦ mulSupport <| f i) (h : ∀ i, SmoothAt I' I (f i) x₀) :
SmoothAt I' I (fun x ↦ ∏ᶠ i, f i x) x₀ :=
contMDiffWithinAt_finprod lf h

@[to_additive]
theorem smooth_finset_prod' (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I (∏ i in t, f i) :=
contMDiff_finset_prod' h
#align smooth_finset_prod' smooth_finset_prod'
#align smooth_finset_sum' smooth_finset_sum'
theorem smoothWithinAt_finset_prod' (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) :
SmoothWithinAt I' I (∏ i in t, f i) s x :=
contMDiffWithinAt_finset_prod' h
#align smooth_within_at_finset_prod' smoothWithinAt_finset_prod'
#align smooth_within_at_finset_sum' smoothWithinAt_finset_sum'

@[to_additive]
theorem smoothWithinAt_finset_prod (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) :
Expand All @@ -401,47 +449,47 @@ theorem smoothWithinAt_finset_prod (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s
#align smooth_within_at_finset_prod smoothWithinAt_finset_prod
#align smooth_within_at_finset_sum smoothWithinAt_finset_sum

@[to_additive]
theorem smoothAt_finset_prod' (h : ∀ i ∈ t, SmoothAt I' I (f i) x) :
SmoothAt I' I (∏ i in t, f i) x :=
contMDiffAt_finset_prod' h
#align smooth_at_finset_prod' smoothAt_finset_prod'
#align smooth_at_finset_sum' smoothAt_finset_sum'

@[to_additive]
theorem smoothAt_finset_prod (h : ∀ i ∈ t, SmoothAt I' I (f i) x) :
SmoothAt I' I (fun x => ∏ i in t, f i x) x :=
contMDiffAt_finset_prod h
#align smooth_at_finset_prod smoothAt_finset_prod
#align smooth_at_finset_sum smoothAt_finset_sum

@[to_additive]
theorem smoothOn_finset_prod' (h : ∀ i ∈ t, SmoothOn I' I (f i) s) :
SmoothOn I' I (∏ i in t, f i) s :=
contMDiffOn_finset_prod' h
#align smooth_on_finset_prod' smoothOn_finset_prod'
#align smooth_on_finset_sum' smoothOn_finset_sum'

@[to_additive]
theorem smoothOn_finset_prod (h : ∀ i ∈ t, SmoothOn I' I (f i) s) :
SmoothOn I' I (fun x => ∏ i in t, f i x) s :=
contMDiffOn_finset_prod h
#align smooth_on_finset_prod smoothOn_finset_prod
#align smooth_on_finset_sum smoothOn_finset_sum

@[to_additive]
theorem smooth_finset_prod' (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I (∏ i in t, f i) :=
contMDiff_finset_prod' h
#align smooth_finset_prod' smooth_finset_prod'
#align smooth_finset_sum' smooth_finset_sum'

@[to_additive]
theorem smooth_finset_prod (h : ∀ i ∈ t, Smooth I' I (f i)) :
Smooth I' I fun x => ∏ i in t, f i x :=
contMDiff_finset_prod h
#align smooth_finset_prod smooth_finset_prod
#align smooth_finset_sum smooth_finset_sum

open Function Filter

@[to_additive]
theorem contMDiff_finprod (h : ∀ i, ContMDiff I' I n (f i))
(hfin : LocallyFinite fun i => mulSupport (f i)) : ContMDiff I' I n fun x => ∏ᶠ i, f i x := by
intro x
rcases finprod_eventually_eq_prod hfin x with ⟨s, hs⟩
exact (contMDiff_finset_prod (fun i _ => h i) x).congr_of_eventuallyEq hs
#align cont_mdiff_finprod contMDiff_finprod
#align cont_mdiff_finsum contMDiff_finsum

@[to_additive]
theorem contMDiff_finprod_cond (hc : ∀ i, p i → ContMDiff I' I n (f i))
(hf : LocallyFinite fun i => mulSupport (f i)) :
ContMDiff I' I n fun x => ∏ᶠ (i) (_ : p i), f i x := by
simp only [← finprod_subtype_eq_finprod_cond]
exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
#align cont_mdiff_finprod_cond contMDiff_finprod_cond
#align cont_mdiff_finsum_cond contMDiff_finsum_cond

@[to_additive]
theorem smooth_finprod (h : ∀ i, Smooth I' I (f i))
(hfin : LocallyFinite fun i => mulSupport (f i)) : Smooth I' I fun x => ∏ᶠ i, f i x :=
Expand Down

0 comments on commit a686ba8

Please sign in to comment.