Theorems · Definition · functional analysis

LineDeriv.laplacianCLM

(R : Type u_4) →
  (E : Type u_6) →
    (V₁ : Type u_8) →
      {V₂ : Type u_9} →
        {V₃ : Type u_10} →
          [inst : LineDeriv E V₁ V₂] →
            [inst_1 : LineDeriv E V₂ V₃] →
              [inst_2 : AddCommGroup V₁] →
                [inst_3 : AddCommGroup V₂] →
                  [inst_4 : AddCommGroup V₃] →
                    [inst_5 : NormedAddCommGroup E] →
                      [inst_6 : InnerProductSpace ℝ E] →
                        [FiniteDimensional ℝ E] →
                          [inst_8 : CommRing R] →
                            [inst_9 : Module R V₁] →
                              [inst_10 : Module R V₂] →
                                [inst_11 : Module R V₃] →
                                  [inst_12 : TopologicalSpace V₁] →
                                    [inst_13 : TopologicalSpace V₂] →
                                      [inst_14 : TopologicalSpace V₃] →
                                        [IsTopologicalAddGroup V₃] →
                                          [LineDerivAdd E V₁ V₂] →
                                            [LineDerivSMul R E V₁ V₂] →
                                              [ContinuousLineDeriv E V₁ V₂] →
                                                [LineDerivAdd E V₂ V₃] →
                                                  [LineDerivSMul R E V₂ V₃] →
                                                    [ContinuousLineDeriv E V₂ V₃] → V₁ →L[R] V₃

The Laplacian defined by iterated lineDerivOp as a continuous linear map.

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

4 results in Mathlib

Foundations

Depth 241 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LineDerivLineDerivAddCommGroupAddCommGroupAddCommGroupNormedAddCommGroupInnerProductSpaceFiniteDimensionalCommRingModuleModuleModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupLineDerivAddLineDerivSMulContinuousLineDerivLineDerivAddLineDerivSMulContinuousLineDeriv