Documentation

MIPRE.Foundations.Introspection.AuxiliaryDualKernel

Coordinate-independent kernel tests for auxiliary dual answers #

The semantic dual uses a chosen local enumeration, but equality of its outputs is characterized intrinsically by the ambient dot product. The general finite index API permits coordinate transport without transporting chosen complements.

source
noncomputable def MIPRE.Introspection.AuxiliaryDual.registerDual {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) :
(ι → F) →ₗ[F] ι → F

The semantic local dual, inserted back into the ambient register.

Equations
Instances For
    source
    theorem MIPRE.Introspection.AuxiliaryDual.coordinateInsert_injective {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {S : Finset ι} :
    Function.Injective ⇑(coordinateInsert S)
    source
    theorem MIPRE.Introspection.AuxiliaryDual.coordinate_dot_sum {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (x y : ι → F) :
    ((CL.dotForm F (Fintype.card ↥S)) ((coordinateRestrict S) x)) ((coordinateRestrict S) y) = ∑ i : ι, x i * (CL.proj S) y i
    source
    theorem MIPRE.Introspection.AuxiliaryDual.coordinateLinear_zero_iff {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (x : ι → F) :
    (coordinateLinear L) ((coordinateRestrict S) x) = 0 ↔ L x = 0
    source
    theorem MIPRE.Introspection.AuxiliaryDual.registerDual_zero_iff_local {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (x : ι → F) :
    (registerDual L) x = 0 ↔ (coordinateRestrict S) x ∈ CL.perp (coordinateLinear L).ker
    source
    theorem MIPRE.Introspection.AuxiliaryDual.registerDual_zero_iff_dot {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (x : ι → F) :
    (registerDual L) x = 0 ↔ ∀ (y : ι → F), L y = 0 → ∑ i : ι, y i * (CL.proj S) x i = 0

    Intrinsic kernel characterization on any finite ambient coordinate type.

    source
    theorem MIPRE.Introspection.AuxiliaryDual.registerDual_eq_iff_dot {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (x y : ι → F) :
    (registerDual L) x = (registerDual L) y ↔ ∀ (z : ι → F), L z = 0 → ∑ i : ι, z i * (CL.proj S) (x - y) i = 0
    source
    theorem MIPRE.Introspection.AuxiliaryDual.registerDual_idempotent {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (x : ι → F) :
    (registerDual L) ((registerDual L) x) = (registerDual L) x
    source
    theorem MIPRE.Introspection.AuxiliaryDual.registerDual_zero_iff {F : Type u_1} [Field F] {n : ℕ} {T : Finset (Fin n)} (L : CL.RegLinear F T) (x : Fin n → F) :
    (registerDual L) x = 0 ↔ (CL.proj T) x ∈ CL.perp L.toLinearMap.ker

    The local-coordinate dual kernel can be tested on a projected ambient vector.

    source
    theorem MIPRE.Introspection.AuxiliaryDual.registerDual_eq_iff {F : Type u_1} [Field F] {n : ℕ} {T : Finset (Fin n)} (L : CL.RegLinear F T) (x y : Fin n → F) :
    (registerDual L) x = (registerDual L) y ↔ (CL.proj T) (x - y) ∈ CL.perp L.toLinearMap.ker

    Comparing two semantic dual labels is an ambient row-space membership test.