Documentation

LeanPool.BollobasNikiforov.Kernel.Data

Three-column kernel data #

Feature vectors, the Gram matrix π’œ, moment scalars, and the auxiliary functions of docs/sol.tex Β§3 (sec:kernel, eq:functions). Coordinates of ℝ³ are numbered 0,1,2.

source
noncomputable def BollobasNikiforov.v (t : ℝ) :
Fin 3 β†’ ℝ

Feature vector v(t) = (1, -√2 t, tΒ²)α΅€.

Equations
Instances For
    source
    noncomputable def BollobasNikiforov.b (x : ℝ) :
    Fin 3 β†’ ℝ

    Feature vector b(x) = (xΒ², √2 x, 1)α΅€.

    Equations
    Instances For
      source
      def BollobasNikiforov.truncSq (ti x : ℝ) :
      ℝ

      Truncated square aα΅’(x) = (x - tα΅’)β‚ŠΒ².

      Equations
      Instances For
        source
        theorem BollobasNikiforov.isHermitian_vecMulVec_self (w : Fin 3 β†’ ℝ) :
        (Matrix.vecMulVec w w).IsHermitian

        The outer product v vα΅€ is Hermitian.

        source
        theorem BollobasNikiforov.mulVec_vecMulVec_self (w x : Fin 3 β†’ ℝ) :
        (Matrix.vecMulVec w w).mulVec x = (w ⬝α΅₯ x) β€’ w

        (v vα΅€) x = (v ⬝ x) v.

        source
        theorem BollobasNikiforov.dotProduct_mulVec_vecMulVec_self (w x : Fin 3 β†’ ℝ) :
        x ⬝α΅₯ (Matrix.vecMulVec w w).mulVec x = (w ⬝α΅₯ x) ^ 2

        The quadratic form of an outer product is a square: x ⬝ (v vα΅€) x = (v ⬝ x)Β².

        source
        theorem BollobasNikiforov.posSemidef_vecMulVec_self_fin3 (w : Fin 3 β†’ ℝ) :
        (Matrix.vecMulVec w w).PosSemidef

        The outer product v vα΅€ is positive semidefinite.

        source
        @[simp]
        theorem BollobasNikiforov.v_zero (s : ℝ) :
        v s 0 = 1
        source
        @[simp]
        theorem BollobasNikiforov.v_one (s : ℝ) :
        v s 1 = -√2 * s
        source
        @[simp]
        theorem BollobasNikiforov.v_two (s : ℝ) :
        v s 2 = s ^ 2
        source
        noncomputable def BollobasNikiforov.π’œ {k : β„•} (t q : Fin k β†’ ℝ) :
        Matrix (Fin 3) (Fin 3) ℝ

        Gram matrix π’œ = I₃ + βˆ‘α΅’ qα΅’ v(tα΅’) v(tα΅’)α΅€.

        Equations
        Instances For
          source
          theorem BollobasNikiforov.π’œ_posDef {k : β„•} (t q : Fin k β†’ ℝ) (hq : βˆ€ (i : Fin k), 0 < q i) :
          (π’œ t q).PosDef

          π’œ is positive definite: the identity is PD and each summand is PSD.

          source
          theorem BollobasNikiforov.π’œ_isUnit {k : β„•} (t q : Fin k β†’ ℝ) (hq : βˆ€ (i : Fin k), 0 < q i) :
          IsUnit (π’œ t q)

          Positive definite matrices are invertible.

          source
          def BollobasNikiforov.m {k : β„•} (t q : Fin k β†’ ℝ) (j : β„•) :
          ℝ

          Moments mβ±Ό = βˆ‘α΅’ qα΅’ tα΅’Κ².

          Equations
          Instances For
            source
            theorem BollobasNikiforov.m_zero {k : β„•} (t q : Fin k β†’ ℝ) :
            m t q 0 = βˆ‘ i : Fin k, q i
            source
            def BollobasNikiforov.a0 {k : β„•} (t q : Fin k β†’ ℝ) :
            ℝ

            Scalar aβ‚€ = 1 + mβ‚€.

            Equations
            Instances For
              source
              def BollobasNikiforov.D2 {k : β„•} (t q : Fin k β†’ ℝ) :
              ℝ

              Scalar Dβ‚‚ = aβ‚€(1 + 2 mβ‚‚) - 2 m₁².

              Equations
              Instances For
                source
                noncomputable def BollobasNikiforov.Ξ” {k : β„•} (t q : Fin k β†’ ℝ) :
                ℝ

                Scalar Ξ” = det π’œ.

                Equations
                Instances For
                  source
                  noncomputable def BollobasNikiforov.Vvec {k : β„•} (t q : Fin k β†’ ℝ) :
                  Fin 3 β†’ ℝ

                  Vector V = π’œ eβ‚€.

                  Equations
                  Instances For

                    KR04: principal minors of π’œ #

                    source
                    theorem BollobasNikiforov.π’œ_apply {k : β„•} (t q : Fin k β†’ ℝ) (i j : Fin 3) :
                    π’œ t q i j = (if i = j then 1 else 0) + βˆ‘ r : Fin k, q r * v (t r) i * v (t r) j
                    source
                    theorem BollobasNikiforov.π’œ_00 {k : β„•} (t q : Fin k β†’ ℝ) :
                    π’œ t q 0 0 = a0 t q
                    source
                    theorem BollobasNikiforov.π’œ_11 {k : β„•} (t q : Fin k β†’ ℝ) :
                    π’œ t q 1 1 = 1 + 2 * m t q 2
                    source
                    theorem BollobasNikiforov.π’œ_01 {k : β„•} (t q : Fin k β†’ ℝ) :
                    π’œ t q 0 1 = -√2 * m t q 1
                    source
                    theorem BollobasNikiforov.π’œ_10 {k : β„•} (t q : Fin k β†’ ℝ) :
                    π’œ t q 1 0 = -√2 * m t q 1
                    source
                    theorem BollobasNikiforov.D2_eq_det_leading {k : β„•} (t q : Fin k β†’ ℝ) :
                    D2 t q = ((π’œ t q).submatrix Fin.castSucc Fin.castSucc).det

                    Dβ‚‚ is the leading 2Γ—2 principal minor of π’œ.

                    source
                    theorem BollobasNikiforov.Ξ”_pos {k : β„•} (t q : Fin k β†’ ℝ) (hq : βˆ€ (i : Fin k), 0 < q i) :
                    0 < Ξ” t q
                    source
                    theorem BollobasNikiforov.D2_pos {k : β„•} (t q : Fin k β†’ ℝ) (hq : βˆ€ (i : Fin k), 0 < q i) :
                    0 < D2 t q

                    KR05: auxiliary functions #

                    source
                    def BollobasNikiforov.h {k : β„•} (t q : Fin k β†’ ℝ) (x : ℝ) :
                    ℝ

                    h(x) = βˆ‘α΅’ qα΅’ aα΅’(x).

                    Equations
                    Instances For
                      source
                      def BollobasNikiforov.h1 {k : β„•} (t q : Fin k β†’ ℝ) (x : ℝ) :
                      ℝ

                      h₁(x) = βˆ‘α΅’ qα΅’ tα΅’ aα΅’(x).

                      Equations
                      Instances For
                        source
                        noncomputable def BollobasNikiforov.bhat {k : β„•} (t q : Fin k β†’ ℝ) (x : ℝ) :
                        Fin 3 β†’ ℝ

                        bΜ‚(x) = b(x) + βˆ‘α΅’ qα΅’ aα΅’(x) v(tα΅’).

                        Equations
                        Instances For
                          source
                          noncomputable def BollobasNikiforov.U {k : β„•} (t q : Fin k β†’ ℝ) (Ξ³ x : ℝ) :
                          Fin 3 β†’ ℝ

                          U(x) = bΜ‚(x) + (h(x)/Ξ³) V.

                          Equations
                          Instances For
                            source
                            noncomputable def BollobasNikiforov.𝒦Mat {k : β„•} (t q : Fin k β†’ ℝ) (Ξ³ : ℝ) :
                            Matrix (Fin 3) (Fin 3) ℝ

                            The Gram update π’œ + VVα΅€/Ξ³ before inversion.

                            Equations
                            Instances For
                              source
                              theorem BollobasNikiforov.𝒦Mat_posDef {k : β„•} (t q : Fin k β†’ ℝ) (Ξ³ : ℝ) (hq : βˆ€ (i : Fin k), 0 < q i) (hΞ³ : 0 < Ξ³) :
                              (𝒦Mat t q Ξ³).PosDef
                              source
                              theorem BollobasNikiforov.𝒦Mat_isUnit {k : β„•} (t q : Fin k β†’ ℝ) (Ξ³ : ℝ) (hq : βˆ€ (i : Fin k), 0 < q i) (hΞ³ : 0 < Ξ³) :
                              IsUnit (𝒦Mat t q Ξ³)
                              source
                              noncomputable def BollobasNikiforov.𝒦 {k : β„•} (t q : Fin k β†’ ℝ) (Ξ³ : ℝ) :
                              Matrix (Fin 3) (Fin 3) ℝ

                              𝒦 = (π’œ + VVα΅€/Ξ³)⁻¹.

                              Equations
                              Instances For
                                source
                                noncomputable def BollobasNikiforov.N {k : β„•} (t q : Fin k β†’ ℝ) (x : ℝ) :
                                ℝ

                                N(x) = Ξ” eβ‚‚α΅€ π’œβ»ΒΉ bΜ‚(x).

                                Equations
                                Instances For
                                  source
                                  def BollobasNikiforov.P {k : β„•} (t q : Fin k β†’ ℝ) (x : ℝ) :
                                  ℝ

                                  P(x) = aβ‚€ x + m₁ xΒ² + m₁ h(x) βˆ’ aβ‚€ h₁(x).

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    def BollobasNikiforov.Z {k : β„•} (t q : Fin k β†’ ℝ) (Ξ³ x : ℝ) :
                                    ℝ

                                    Z(x) = Ξ³ xΒ² + (Ξ³ + aβ‚€) h(x).

                                    Equations
                                    Instances For

                                      KR06: π’œβ»ΒΉ V = eβ‚€ #

                                      source
                                      theorem BollobasNikiforov.π’œ_inv_mulVec_Vvec {k : β„•} (t q : Fin k β†’ ℝ) (hq : βˆ€ (i : Fin k), 0 < q i) :
                                      (π’œ t q)⁻¹.mulVec (Vvec t q) = Pi.single 0 1