Theorems · Definition · functional analysis

LineDeriv.bilinearLineDerivTwo

(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 : CommRing R] →
                      [inst_6 : AddCommGroup E] →
                        [inst_7 : Module R E] →
                          [inst_8 : Module R V₂] →
                            [inst_9 : Module R V₃] →
                              [LineDerivAdd E V₂ V₃] →
                                [LineDerivAdd E V₁ V₂] →
                                  [LineDerivSMul R E V₂ V₃] →
                                    [LineDerivLeftSMul R E V₁ V₂] →
                                      [LineDerivLeftSMul R E V₂ V₃] → V₁ → E →ₗ[R] E →ₗ[R] V₃

The second derivative in terms lineDerivOp as a bilinear map. Mainly used to give an abstract definition of the Laplacian.

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

0 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Quot.sound

Assumes

LineDerivLineDerivAddCommGroupAddCommGroupAddCommGroupCommRingAddCommGroupModuleModuleModuleLineDerivAddLineDerivAddLineDerivSMulLineDerivLeftSMulLineDerivLeftSMul