Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: finite products/sums of differentiable maps into smooth commutative monoids are differentiable #9775

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: finite products/sums of differentiable maps into smooth commutative monoids are differentiable #9775

Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
4b5ef7c
Add some docstrings.
grunweg Jan 15, 2024
23a1d27
Tweak section names, add comments explaining them.
grunweg Jan 15, 2024
31e3be5
Main doc: reflow lines.
grunweg Jan 15, 2024
ff339e4
Extend main module docstring.
grunweg Jan 15, 2024
b4198a5
Review comments: extend documentation.
grunweg Jan 16, 2024
fda1584
Split main definitions and results; clarify additive vs multiplicativ…
grunweg Jan 16, 2024
3001890
Point to other instance.
grunweg Jan 16, 2024
ad94f27
Snapshot.
grunweg Jan 16, 2024
037fcda
Merge branch 'master' into MR-sphere-eversion-LieGroup2
grunweg Jan 16, 2024
914399c
Move to Monoid file.
grunweg Jan 24, 2024
6e44518
chore: re-order lemmas into logical order.
grunweg Jan 24, 2024
64056c1
Open Function for mulSupport.
grunweg Jan 24, 2024
1a668f6
Small golf; add contMDiffOn_finprod.
grunweg Jan 24, 2024
acb4ed5
Update Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
ocfnash Jan 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ groups here are not necessarily finite dimensional.
is smooth at all points at which `f` doesn't vanish.
``ContMDiff.div₀` and variants: if also `SmoothMul N` (i.e., `N` is a Lie group except possibly
for smoothness of inversion at `0`), similar results hold for point-wise division.

ocfnash marked this conversation as resolved.
Show resolved Hide resolved
* `normedSpaceLieAddGroup` : a normed vector space over a nontrivially normed field
is an additive Lie group.
* `Instances/UnitsOfNormedAlgebra` shows that the group of units of a complete normed `𝕜`-algebra
Expand Down
178 changes: 113 additions & 65 deletions Mathlib/Geometry/Manifold/Algebra/Monoid.lean
View file
Open in desktop
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
Loading