mathlibdocumentation

geometry.manifold.algebra.monoid

Smooth monoid #

A smooth monoid is a monoid that is also a smooth manifold, in which multiplication is a smooth map of the product manifold G × G into G.

In this file we define the basic structures to talk about smooth monoids: has_smooth_mul and its additive counterpart has_smooth_add. These structures are general enough to also talk about smooth semigroups.

1. All smooth algebraic structures on G are Prop-valued classes that extend smooth_manifold_with_corners I G. This way we save users from adding both [smooth_manifold_with_corners I G] and [has_smooth_mul I G] to the assumptions. While many API lemmas hold true without the smooth_manifold_with_corners I G assumption, we're not aware of a mathematically interesting monoid on a topological manifold such that (a) the space is not a smooth_manifold_with_corners; (b) the multiplication is smooth at (a, b) in the charts ext_chart_at I a, ext_chart_at I b, ext_chart_at I (a * b).

2. Because of model_prod we can't assume, e.g., that a lie_group is modelled on 𝓘(𝕜, E). So, we formulate the definitions and lemmas for any model.

3. While smoothness of an operation implies its continuity, lemmas like has_continuous_mul_of_smooth can't be instances becausen otherwise Lean would have to search for has_smooth_mul I G with unknown 𝕜, E, H, and I : model_with_corners 𝕜 E H. If users needs [has_continuous_mul G] in a proof about a smooth monoid, then they need to either add [has_continuous_mul G] as an assumption (worse) or use haveI in the proof (better).

@[class]
structure has_smooth_add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) (G : Type u_4) [has_add G] [ G] :
Prop
• to_smooth_manifold_with_corners :
• smooth_add : smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)

Basic hypothesis to talk about a smooth (Lie) additive monoid or a smooth additive semigroup. A smooth additive monoid over α, for example, is obtained by requiring both the instances add_monoid α and has_smooth_add α.

Instances of this typeclass
@[class]
structure has_smooth_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) (G : Type u_4) [has_mul G] [ G] :
Prop
• to_smooth_manifold_with_corners :
• smooth_mul : smooth (I.prod I) I (λ (p : G × G), p.fst * p.snd)

Basic hypothesis to talk about a smooth (Lie) monoid or a smooth semigroup. A smooth monoid over G, for example, is obtained by requiring both the instances monoid G and has_smooth_mul I G.

Instances of this typeclass
theorem smooth_add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_add G] [ G] [ G] :
smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)
theorem smooth_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] :
smooth (I.prod I) I (λ (p : G × G), p.fst * p.snd)
theorem has_continuous_add_of_smooth {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_add G] [ G] [ G] :

If the addition is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

theorem has_continuous_mul_of_smooth {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] :

If the multiplication is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

theorem cont_mdiff_within_at.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} {x : M} {n : ℕ∞} (hf : n f s x) (hg : n g s x) :
n (f + g) s x
theorem cont_mdiff_within_at.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} {x : M} {n : ℕ∞} (hf : n f s x) (hg : n g s x) :
n (f * g) s x
theorem cont_mdiff_at.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {x : M} {n : ℕ∞} (hf : I n f x) (hg : I n g x) :
I n (f * g) x
theorem cont_mdiff_at.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {x : M} {n : ℕ∞} (hf : I n f x) (hg : I n g x) :
I n (f + g) x
theorem cont_mdiff_on.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} {n : ℕ∞} (hf : I n f s) (hg : I n g s) :
I n (f * g) s
theorem cont_mdiff_on.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} {n : ℕ∞} (hf : I n f s) (hg : I n g s) :
I n (f + g) s
theorem cont_mdiff.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {n : ℕ∞} (hf : I n f) (hg : I n g) :
I n (f + g)
theorem cont_mdiff.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {n : ℕ∞} (hf : I n f) (hg : I n g) :
I n (f * g)
theorem smooth_within_at.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} {x : M} (hf : I f s x) (hg : I g s x) :
I (f * g) s x
theorem smooth_within_at.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} {x : M} (hf : I f s x) (hg : I g s x) :
I (f + g) s x
theorem smooth_at.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {x : M} (hf : I f x) (hg : I g x) :
I (f * g) x
theorem smooth_at.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {x : M} (hf : I f x) (hg : I g x) :
I (f + g) x
theorem smooth_on.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} (hf : I f s) (hg : I g s) :
I (f * g) s
theorem smooth_on.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} (hf : I f s) (hg : I g s) :
I (f + g) s
theorem smooth.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} (hf : smooth I' I f) (hg : smooth I' I g) :
smooth I' I (f * g)
theorem smooth.add {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} (hf : smooth I' I f) (hg : smooth I' I g) :
smooth I' I (f + g)
theorem smooth_mul_left {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {a : G} :
I (λ (b : G), a * b)
theorem smooth_add_left {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {a : G} :
I (λ (b : G), a + b)
theorem smooth_mul_right {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {a : G} :
I (λ (b : G), b * a)
theorem smooth_add_right {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {a : G} :
I (λ (b : G), b + a)
def smooth_left_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g : G) :
G G

Left multiplication by g. It is meant to mimic the usual notation in Lie groups. Lemmas involving smooth_left_mul with the notation 𝑳 usually use L instead of 𝑳 in the names.

Equations
def smooth_right_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g : G) :
G G

Right multiplication by g. It is meant to mimic the usual notation in Lie groups. Lemmas involving smooth_right_mul with the notation 𝑹 usually use R instead of 𝑹 in the names.

Equations
@[simp]
theorem L_apply {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g h : G) :
g) h = g * h
@[simp]
theorem R_apply {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g h : G) :
g) h = h * g
@[simp]
theorem L_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [semigroup G] [ G] [ G] (g h : G) :
(g * h) = g).comp h)
@[simp]
theorem R_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G : Type u_4} [semigroup G] [ G] [ G] (g h : G) :
(g * h) = h).comp g)
theorem smooth_left_mul_one {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G' : Type u_8} [monoid G'] [ G'] [ G'] (g' : G') :
g') 1 = g'
theorem smooth_right_mul_one {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] (I : H) {G' : Type u_8} [monoid G'] [ G'] [ G'] (g' : G') :
g') 1 = g'
@[protected, instance]
def has_smooth_add.sum {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) (G : Type u_4) [ G] [has_add G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') (G' : Type u_7) [ G'] [has_add G'] [ G'] :
has_smooth_add (I.prod I') (G × G')
@[protected, instance]
def has_smooth_mul.prod {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) (G : Type u_4) [ G] [has_mul G] [ G] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') (G' : Type u_7) [ G'] [has_mul G'] [ G'] :
has_smooth_mul (I.prod I') (G × G')
theorem smooth_pow {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] (n : ) :
I (λ (a : G), a ^ n)
structure smooth_add_monoid_morphism {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {H' : Type u_5} {E' : Type u_6} [ E'] (I : H) (I' : H') (G : Type u_8) [ G] [add_monoid G] [ G] (G' : Type u_9) [ G'] [add_monoid G'] [ G'] :
Type (max u_8 u_9)

Instances for smooth_add_monoid_morphism
structure smooth_monoid_morphism {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {H' : Type u_5} {E' : Type u_6} [ E'] (I : H) (I' : H') (G : Type u_8) [ G] [monoid G] [ G] (G' : Type u_9) [ G'] [monoid G'] [ G'] :
Type (max u_8 u_9)

Morphism of smooth monoids.

Instances for smooth_monoid_morphism
@[protected, instance]
def smooth_add_monoid_morphism.has_zero {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [add_monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [ E'] {I' : H'} {G' : Type u_7} [add_monoid G'] [ G'] [ G'] :
has_zero G G')
Equations
@[protected, instance]
def smooth_monoid_morphism.has_one {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [ E'] {I' : H'} {G' : Type u_7} [monoid G'] [ G'] [ G'] :
has_one G G')
Equations
@[protected, instance]
def smooth_add_monoid_morphism.inhabited {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [add_monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [ E'] {I' : H'} {G' : Type u_7} [add_monoid G'] [ G'] [ G'] :
inhabited G G')
Equations
@[protected, instance]
def smooth_monoid_morphism.inhabited {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [ E'] {I' : H'} {G' : Type u_7} [monoid G'] [ G'] [ G'] :
inhabited G G')
Equations
@[protected, instance]
def smooth_add_monoid_morphism.has_coe_to_fun {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [add_monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [ E'] {I' : H'} {G' : Type u_7} [add_monoid G'] [ G'] [ G'] :
has_coe_to_fun G G') (λ (_x : G'), G → G')
Equations
@[protected, instance]
def smooth_monoid_morphism.has_coe_to_fun {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [ E'] {I' : H'} {G' : Type u_7} [monoid G'] [ G'] [ G'] :
has_coe_to_fun G G') (λ (_x : G G'), G → G')
Equations
theorem cont_mdiff_within_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t n (f i) s x) :
n (t.prod (λ (i : ι), f i)) s x
theorem cont_mdiff_within_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t n (f i) s x) :
n (t.sum (λ (i : ι), f i)) s x
theorem cont_mdiff_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) x) :
I n (t.prod (λ (i : ι), f i)) x
theorem cont_mdiff_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) x) :
I n (t.sum (λ (i : ι), f i)) x
theorem cont_mdiff_on_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) s) :
I n (t.prod (λ (i : ι), f i)) s
theorem cont_mdiff_on_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) s) :
I n (t.sum (λ (i : ι), f i)) s
theorem cont_mdiff_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i)) :
I n (t.sum (λ (i : ι), f i))
theorem cont_mdiff_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i)) :
I n (t.prod (λ (i : ι), f i))
theorem cont_mdiff_within_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t n (f i) s x) :
n (λ (x : M), t.sum (λ (i : ι), f i x)) s x
theorem cont_mdiff_within_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t n (f i) s x) :
n (λ (x : M), t.prod (λ (i : ι), f i x)) s x
theorem cont_mdiff_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) x) :
I n (λ (x : M), t.sum (λ (i : ι), f i x)) x
theorem cont_mdiff_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) x) :
I n (λ (x : M), t.prod (λ (i : ι), f i x)) x
theorem cont_mdiff_on_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) s) :
I n (λ (x : M), t.sum (λ (i : ι), f i x)) s
theorem cont_mdiff_on_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i) s) :
I n (λ (x : M), t.prod (λ (i : ι), f i x)) s
theorem cont_mdiff_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i)) :
I n (λ (x : M), t.sum (λ (i : ι), f i x))
theorem cont_mdiff_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i t I n (f i)) :
I n (λ (x : M), t.prod (λ (i : ι), f i x))
theorem smooth_within_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s x) :
I (t.prod (λ (i : ι), f i)) s x
theorem smooth_within_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s x) :
I (t.sum (λ (i : ι), f i)) s x
theorem smooth_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) x) :
I (t.sum (λ (i : ι), f i)) x
theorem smooth_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) x) :
I (t.prod (λ (i : ι), f i)) x
theorem smooth_on_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s) :
I (t.sum (λ (i : ι), f i)) s
theorem smooth_on_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s) :
I (t.prod (λ (i : ι), f i)) s
theorem smooth_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (t.sum (λ (i : ι), f i))
theorem smooth_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (t.prod (λ (i : ι), f i))
theorem smooth_within_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s x) :
I (λ (x : M), t.sum (λ (i : ι), f i x)) s x
theorem smooth_within_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s x) :
I (λ (x : M), t.prod (λ (i : ι), f i x)) s x
theorem smooth_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) x) :
I (λ (x : M), t.sum (λ (i : ι), f i x)) x
theorem smooth_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) x) :
I (λ (x : M), t.prod (λ (i : ι), f i x)) x
theorem smooth_on_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s) :
I (λ (x : M), t.sum (λ (i : ι), f i x)) s
theorem smooth_on_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i t I (f i) s) :
I (λ (x : M), t.prod (λ (i : ι), f i x)) s
theorem smooth_finset_prod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (λ (x : M), t.prod (λ (i : ι), f i x))
theorem smooth_finset_sum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (λ (x : M), t.sum (λ (i : ι), f i x))
theorem cont_mdiff_finsum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), I n (f i)) (hfin : locally_finite (λ (i : ι), function.support (f i))) :
I n (λ (x : M), finsum (λ (i : ι), f i x))
theorem cont_mdiff_finprod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), I n (f i)) (hfin : locally_finite (λ (i : ι), function.mul_support (f i))) :
I n (λ (x : M), finprod (λ (i : ι), f i x))
theorem cont_mdiff_finprod_cond {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} {n : ℕ∞} {p : ι → Prop} (hc : ∀ (i : ι), p i I n (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
I n (λ (x : M), finprod (λ (i : ι), finprod (λ (hi : p i), f i x)))
theorem cont_mdiff_finsum_cond {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} {n : ℕ∞} {p : ι → Prop} (hc : ∀ (i : ι), p i I n (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
I n (λ (x : M), finsum (λ (i : ι), finsum (λ (hi : p i), f i x)))
theorem smooth_finprod {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} (h : ∀ (i : ι), smooth I' I (f i)) (hfin : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), finprod (λ (i : ι), f i x))
theorem smooth_finsum {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} (h : ∀ (i : ι), smooth I' I (f i)) (hfin : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), finsum (λ (i : ι), f i x))
theorem smooth_finsum_cond {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p ismooth I' I (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), finsum (λ (i : ι), finsum (λ (hi : p i), f i x)))
theorem smooth_finprod_cond {ι : Type u_1} {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [ E] {I : H} {G : Type u_5} [comm_monoid G] [ G] [ G] {E' : Type u_6} [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p ismooth I' I (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), finprod (λ (i : ι), finprod (λ (hi : p i), f i x)))