Documentation

BrownianMotion.Auxiliary.ContinuousBilinForm

Continuous bilinear forms #

@[reducible, inline]
abbrev ContinuousBilinForm (π•œ : Type u_1) (E : Type u_2) [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] :
Type (max u_2 u_1 u_2)
Equations
Instances For
    def ContinuousBilinForm.toBilinForm {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) :

    The underlying bilinear form of a continuous bilinear form

    Equations
    • f.toBilinForm = { toFun := fun (x : E) => ↑(f x), map_add' := β‹―, map_smul' := β‹― }
    Instances For
      @[simp]
      theorem ContinuousBilinForm.toBilinForm_apply {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) (x y : E) :
      (f.toBilinForm x) y = (f x) y
      structure ContinuousBilinForm.IsSymm {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) :

      A continuous bilinear form f is symmetric if for any x, y we have f x y = f y x.

      • map_symm (x y : E) : (f x) y = (f y) x
      Instances For
        theorem ContinuousBilinForm.isSymm_def {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) :
        f.IsSymm ↔ βˆ€ (x y : E), (f x) y = (f y) x
        theorem ContinuousBilinForm.IsSymm.polarization {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] {f : ContinuousBilinForm π•œ E} (x y : E) (hf : f.IsSymm) :
        (f x) y = ((f (x + y)) (x + y) - (f x) x - (f y) y) / 2

        Polarization identity: a symmetric continuous bilinear form can be expressed through values it takes on the diagonal.

        theorem ContinuousBilinForm.ext_of_isSymm {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] {f g : ContinuousBilinForm π•œ E} (hf : f.IsSymm) (hg : g.IsSymm) (h : βˆ€ (x : E), (f x) x = (g x) x) :
        f = g

        A symmetric continuous bilinear form is characterized by the values it takes on the diagonal.

        theorem ContinuousBilinForm.ext_iff_of_isSymm {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] {f g : ContinuousBilinForm π•œ E} (hf : f.IsSymm) (hg : g.IsSymm) :
        f = g ↔ βˆ€ (x : E), (f x) x = (g x) x

        A symmetric continuous bilinear form is characterized by the values it takes on the diagonal.

        theorem ContinuousBilinForm.isSymm_iff_basis {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) (b : Basis n π•œ E) :
        f.IsSymm ↔ βˆ€ (i j : n), (f (b i)) (b j) = (f (b j)) (b i)
        noncomputable def ContinuousBilinForm.toMatrix {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) (b : Basis n π•œ E) [Fintype n] [DecidableEq n] :
        Matrix n n π•œ

        A continuous bilinear map on a finite dimensional space can be represented by a matrix.

        Equations
        Instances For
          @[simp]
          theorem ContinuousBilinForm.toMatrix_apply {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) (b : Basis n π•œ E) [Fintype n] [DecidableEq n] (i j : n) :
          f.toMatrix b i j = (f (b i)) (b j)
          theorem ContinuousBilinForm.dotProduct_toMatrix_mulVec {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) (b : Basis n π•œ E) [Fintype n] [DecidableEq n] (x y : n β†’ π•œ) :
          theorem ContinuousBilinForm.apply_eq_dotProduct_toMatrix_mulVec {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) (b : Basis n π•œ E) [Fintype n] [DecidableEq n] (x y : E) :
          (f x) y = ⇑(b.repr x) ⬝α΅₯ (f.toMatrix b).mulVec ⇑(b.repr y)
          noncomputable def ContinuousBilinForm.ofMatrix {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] [Fintype n] [DecidableEq n] (M : Matrix n n π•œ) (b : Basis n π•œ E) :
          Equations
          Instances For
            theorem ContinuousBilinForm.ofMatrix_apply' {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] [Fintype n] [DecidableEq n] (M : Matrix n n π•œ) (b : Basis n π•œ E) (x y : E) :
            ((ofMatrix M b) x) y = (((Matrix.toBilin b) M) x) y
            theorem ContinuousBilinForm.ofMatrix_apply {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] [Fintype n] [DecidableEq n] (M : Matrix n n π•œ) (b : Basis n π•œ E) (x y : E) :
            ((ofMatrix M b) x) y = ⇑(b.repr x) ⬝α΅₯ M.mulVec ⇑(b.repr y)
            theorem ContinuousBilinForm.ofMatrix_basis {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] [Fintype n] [DecidableEq n] (M : Matrix n n π•œ) (b : Basis n π•œ E) (i j : n) :
            ((ofMatrix M b) (b i)) (b j) = M i j
            theorem ContinuousBilinForm.ofMatrix_orthonormalBasis {π•œ : Type u_1} {n : Type u_3} [RCLike π•œ] [Fintype n] [DecidableEq n] (M : Matrix n n π•œ) {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace π•œ E] (b : OrthonormalBasis n π•œ E) (i j : n) :
            ((ofMatrix M b.toBasis) (b i)) (b j) = M i j
            theorem ContinuousBilinForm.toMatrix_ofMatrix {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) [Fintype n] [DecidableEq n] (b : Basis n π•œ E) :
            ofMatrix (f.toMatrix b) b = f
            theorem ContinuousBilinForm.ofMatrix_toMatrix {π•œ : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] [Fintype n] [DecidableEq n] (M : Matrix n n π•œ) (b : Basis n π•œ E) :
            (ofMatrix M b).toMatrix b = M
            structure ContinuousBilinForm.IsPos {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) :

            A continuous bilinear map f is positive if for any 0 ≀ x, 0 ≀ re (f x x)

            Instances For
              theorem ContinuousBilinForm.isPos_def {π•œ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike π•œ] [NormedSpace π•œ E] (f : ContinuousBilinForm π•œ E) :
              f.IsPos ↔ βˆ€ (x : E), 0 ≀ RCLike.re ((f x) x)

              A continuous bilinear map is positive semidefinite if it is symmetric and positive. We only define it for the real field, because for the complex case we may want to consider sesquilinear forms instead.

              Instances For

                The inner product as continuous bilinear form.Β 

                Equations
                Instances For