Documentation

SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm

Germs of smooth functions #

under construction: might need further refactoring to be usable!

source
theorem SmoothMap.coe_prod {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_10} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' (β†‘βŠ€) G] {ΞΉ : Type u_11} (f : ΞΉ β†’ ContMDiffMap I I' N G β†‘βŠ€) (s : Finset ΞΉ) :
⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)
source
theorem SmoothMap.coe_sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {G : Type u_10} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffAdd I' (β†‘βŠ€) G] {ΞΉ : Type u_11} (f : ΞΉ β†’ ContMDiffMap I I' N G β†‘βŠ€) (s : Finset ΞΉ) :
⇑(βˆ‘ i ∈ s, f i) = βˆ‘ i ∈ s, ⇑(f i)
source
def RingHom.germOfContMDiffMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {N : Type u_5} [TopologicalSpace N] [ChartedSpace H N] (x : N) :
ContMDiffMap I (modelWithCornersSelf ℝ ℝ) N ℝ β†‘βŠ€ β†’+* (nhds x).Germ ℝ

The map C^∞(N, ℝ) β†’ Germ (𝓝 x) ℝ as a ring homomorphism.

Equations
Instances For
    source
    def smoothGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {N : Type u_5} [TopologicalSpace N] [ChartedSpace H N] (x : N) :
    Subring ((nhds x).Germ ℝ)

    All germs of smooth functions N β†’ ℝ at x : N, as a subring of Germ (𝓝 x) ℝ.

    Equations
    Instances For
      source
      instance instCoeContMDiffMapRealModelWithCornersSelfSomeENatTopSubtypeGermNhdsMemSubringSmoothGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {N : Type u_5} [TopologicalSpace N] [ChartedSpace H N] (x : N) :
      Coe (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) N ℝ β†‘βŠ€) β†₯(smoothGerm I x)
      Equations
      source
      @[simp]
      theorem smoothGerm.coe_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {N : Type u_5} [TopologicalSpace N] [ChartedSpace H N] (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) N ℝ β†‘βŠ€) (x : N) :
      β†‘βŸ¨β†‘β‡‘f, β‹―βŸ© = ↑⇑f
      source
      @[simp]
      theorem smoothGerm.coe_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {N : Type u_5} [TopologicalSpace N] [ChartedSpace H N] {ΞΉ : Type u_11} (f : ΞΉ β†’ ContMDiffMap I (modelWithCornersSelf ℝ ℝ) N ℝ β†‘βŠ€) (s : Finset ΞΉ) (x : N) :
      βŸ¨β†‘β‡‘(βˆ‘ i ∈ s, f i), β‹―βŸ© = βˆ‘ i ∈ s, βŸ¨β†‘β‡‘(f i), β‹―βŸ©
      source
      @[simp]
      theorem smoothGerm.coe_eq_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {N : Type u_5} [TopologicalSpace N] [ChartedSpace H N] (f g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) N ℝ β†‘βŠ€) {x : N} (h : βˆ€αΆ  (y : N) in nhds x, f y = g y) :
      βŸ¨β†‘β‡‘f, β‹―βŸ© = βŸ¨β†‘β‡‘g, β‹―βŸ©
      source
      def smoothGerm.valueOrderRingHom {G : Type u_6} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type u_7} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type u_8} [TopologicalSpace N] [ChartedSpace HG N] (x : N) :
      β†₯(smoothGerm IG x) β†’+*o ℝ
      Equations
      Instances For
        source
        def smoothGerm.valueRingHom {G : Type u_6} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type u_7} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type u_8} [TopologicalSpace N] [ChartedSpace HG N] (x : N) :
        β†₯(smoothGerm IG x) β†’+* ℝ
        Equations
        Instances For
          source
          theorem smoothGerm.valueOrderRingHom_toRingHom {G : Type u_6} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type u_7} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type u_8} [TopologicalSpace N] [ChartedSpace HG N] (x : N) :
          (valueOrderRingHom IG x).toRingHom = valueRingHom IG x
          source
          def Filter.Germ.valueβ‚›β‚— {G : Type u_6} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type u_7} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type u_8} [TopologicalSpace N] [ChartedSpace HG N] {F : Type u_9} [AddCommMonoid F] [Module ℝ F] (x : N) :
          (nhds x).Germ F β†’β‚›β‚—[smoothGerm.valueRingHom IG x] F
          Equations
          Instances For
            source
            def Filter.Germ.ContMDiffAt' {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_6} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type u_7} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type u_8} [TopologicalSpace N] [ChartedSpace HG N] {x : M} (Ο† : (nhds x).Germ N) (n : WithTop β„•βˆž) :
            Prop
            Equations
            Instances For
              source
              def Filter.Germ.ContMDiffAt {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] {x : M} (Ο† : (nhds x).Germ F) (n : WithTop β„•βˆž) :
              Prop

              The predicate selecting germs of ContMDiffAt functions. TODO: merge with the next def that generalizes target space

              Equations
              Instances For
                source
                def Filter.Germ.mfderiv {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_6} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type u_7} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type u_8} [TopologicalSpace N] [ChartedSpace HG N] {x : M} (Ο† : (nhds x).Germ N) :
                TangentSpace I x β†’L[ℝ] TangentSpace IG Ο†.value
                Equations
                Instances For
                  source
                  theorem smoothGerm.contMDiffAt {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} (Ο† : β†₯(smoothGerm I x)) {n : β„•βˆž} :
                  Filter.Germ.ContMDiffAt I ↑φ ↑n
                  source
                  theorem Filter.Germ.ContMDiffAt.add {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] {x : M} {Ο† ψ : (nhds x).Germ F} {n : β„•βˆž} :
                  Germ.ContMDiffAt I Ο† ↑n β†’ Germ.ContMDiffAt I ψ ↑n β†’ Germ.ContMDiffAt I (Ο† + ψ) ↑n
                  source
                  theorem Filter.Germ.ContMDiffAt.smul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] {x : M} {Ο† : (nhds x).Germ ℝ} {ψ : (nhds x).Germ F} {n : β„•βˆž} :
                  Germ.ContMDiffAt I Ο† ↑n β†’ Germ.ContMDiffAt I ψ ↑n β†’ Germ.ContMDiffAt I (Ο† β€’ ψ) ↑n
                  source
                  theorem Filter.Germ.ContMDiffAt.sum {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] {x : M} {ΞΉ : Type u_9} {s : Finset ΞΉ} {n : β„•βˆž} {f : ΞΉ β†’ (nhds x).Germ F} (h : βˆ€ i ∈ s, Germ.ContMDiffAt I (f i) ↑n) :
                  Germ.ContMDiffAt I (βˆ‘ i ∈ s, f i) ↑n
                  source
                  def Filter.Germ.ContMDiffAtProd {E₁ : Type u_1} {Eβ‚‚ : Type u_2} {F : Type u_3} {H₁ : Type u_4} {M₁ : Type u_5} {Hβ‚‚ : Type u_6} {Mβ‚‚ : Type u_7} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [NormedAddCommGroup Eβ‚‚] [NormedSpace ℝ Eβ‚‚] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H₁] (I₁ : ModelWithCorners ℝ E₁ H₁) [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [TopologicalSpace Hβ‚‚] (Iβ‚‚ : ModelWithCorners ℝ Eβ‚‚ Hβ‚‚) [TopologicalSpace Mβ‚‚] [ChartedSpace Hβ‚‚ Mβ‚‚] {x : M₁} (Ο† : (nhds x).Germ (Mβ‚‚ β†’ F)) (n : β„•βˆž) :
                  Prop
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Filter.Germ.ContMDiffAtProd.add {E₁ : Type u_1} {Eβ‚‚ : Type u_2} {F : Type u_3} {H₁ : Type u_4} {M₁ : Type u_5} {Hβ‚‚ : Type u_6} {Mβ‚‚ : Type u_7} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [NormedAddCommGroup Eβ‚‚] [NormedSpace ℝ Eβ‚‚] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H₁] {I₁ : ModelWithCorners ℝ E₁ H₁} [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [TopologicalSpace Hβ‚‚] {Iβ‚‚ : ModelWithCorners ℝ Eβ‚‚ Hβ‚‚} [TopologicalSpace Mβ‚‚] [ChartedSpace Hβ‚‚ Mβ‚‚] {x : M₁} {Ο† ψ : (nhds x).Germ (Mβ‚‚ β†’ F)} {n : β„•βˆž} :
                    ContMDiffAtProd I₁ Iβ‚‚ Ο† n β†’ ContMDiffAtProd I₁ Iβ‚‚ ψ n β†’ ContMDiffAtProd I₁ Iβ‚‚ (Ο† + ψ) n
                    source
                    theorem Filter.Germ.ContMDiffAtProd.smul {E₁ : Type u_1} {Eβ‚‚ : Type u_2} {F : Type u_3} {H₁ : Type u_4} {M₁ : Type u_5} {Hβ‚‚ : Type u_6} {Mβ‚‚ : Type u_7} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [NormedAddCommGroup Eβ‚‚] [NormedSpace ℝ Eβ‚‚] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H₁] {I₁ : ModelWithCorners ℝ E₁ H₁} [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [TopologicalSpace Hβ‚‚] {Iβ‚‚ : ModelWithCorners ℝ Eβ‚‚ Hβ‚‚} [TopologicalSpace Mβ‚‚] [ChartedSpace Hβ‚‚ Mβ‚‚] {x : M₁} {Ο† : (nhds x).Germ (Mβ‚‚ β†’ ℝ)} {ψ : (nhds x).Germ (Mβ‚‚ β†’ F)} {n : β„•βˆž} :
                    ContMDiffAtProd I₁ Iβ‚‚ Ο† n β†’ ContMDiffAtProd I₁ Iβ‚‚ ψ n β†’ ContMDiffAtProd I₁ Iβ‚‚ (Ο† β€’ ψ) n
                    source
                    theorem Filter.Germ.ContMDiffAt.smul_prod {E₁ : Type u_1} {Eβ‚‚ : Type u_2} {F : Type u_3} {H₁ : Type u_4} {M₁ : Type u_5} {Hβ‚‚ : Type u_6} {Mβ‚‚ : Type u_7} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [NormedAddCommGroup Eβ‚‚] [NormedSpace ℝ Eβ‚‚] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H₁] {I₁ : ModelWithCorners ℝ E₁ H₁} [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [TopologicalSpace Hβ‚‚] {Iβ‚‚ : ModelWithCorners ℝ Eβ‚‚ Hβ‚‚} [TopologicalSpace Mβ‚‚] [ChartedSpace Hβ‚‚ Mβ‚‚] {x : M₁} {Ο† : (nhds x).Germ ℝ} {ψ : (nhds x).Germ (Mβ‚‚ β†’ F)} {n : β„•βˆž} :
                    Germ.ContMDiffAt I₁ Ο† ↑n β†’ ContMDiffAtProd I₁ Iβ‚‚ ψ n β†’ ContMDiffAtProd I₁ Iβ‚‚ (Ο† β€’ ψ) n
                    source
                    theorem Filter.Germ.ContMDiffAtProd.sum {E₁ : Type u_1} {Eβ‚‚ : Type u_2} {F : Type u_3} {H₁ : Type u_4} {M₁ : Type u_5} {Hβ‚‚ : Type u_6} {Mβ‚‚ : Type u_7} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [NormedAddCommGroup Eβ‚‚] [NormedSpace ℝ Eβ‚‚] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H₁] {I₁ : ModelWithCorners ℝ E₁ H₁} [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [TopologicalSpace Hβ‚‚] {Iβ‚‚ : ModelWithCorners ℝ Eβ‚‚ Hβ‚‚} [TopologicalSpace Mβ‚‚] [ChartedSpace Hβ‚‚ Mβ‚‚] {x : M₁} {ΞΉ : Type u_8} {s : Finset ΞΉ} {n : β„•βˆž} {f : ΞΉ β†’ (nhds x).Germ (Mβ‚‚ β†’ F)} (h : βˆ€ i ∈ s, ContMDiffAtProd I₁ Iβ‚‚ (f i) n) :
                    ContMDiffAtProd I₁ Iβ‚‚ (βˆ‘ i ∈ s, f i) n