OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Spectrum/MultiplicativeStates.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative states obtained by normalizing translates of additive states.

  1. def OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate line 17

    Source documentation

    Translate a state by multiplication, then normalize at the unit.

    def normalizedTranslate (z : S) (f : S → ℝ) : S → ℝ :=
…
  2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_continuousOn line 20
  3. def OAI.MatrixMultiplication.AuxiliarySeparation.frozenConstraint line 28
  4. def OAI.MatrixMultiplication.AuxiliarySeparation.frozenSlice line 31
  5. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_isClosed line 34
  6. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenSlice_isClosed line 41
  7. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenSlice_isCompact line 45
  8. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_convex line 49
  9. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenSlice_convex line 56
  10. theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_mem_frozenConstraint line 60
  11. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenSlice_mapsTo_normalizedTranslate line 68
  12. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_value line 74
  13. theorem OAI.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_normalizedTranslate_eq line 78
  14. theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_mem_frozenConstraint line 86
  15. theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_nonzero line 93
  16. theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_mem_frozenConstraint_of_normalized line 99
  17. theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_mem_frozenSlice line 104
  18. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_finite_multiplicative_slice line 111

    Source documentation

    Every finite collection of multiplication identities holds throughout a nonempty compact convex subset that remains invariant under all translates.

    theorem exists_finite_multiplicative_slice {K : Set (S → ℝ)}
    (hKcompact : IsCompact K) (hKconvex : Convex ℝ K) (hKne : K.Nonempty)
    (hKnorm : ∀ f ∈ K, f 1 = 1)
    (hKnonzero : ∀ f ∈ K, ∀ z : S, z ≠ 0 → f z ≠ 0)
    (hKmap : ∀ z : S, z ≠ 0 → MapsTo (normalizedTranslate z) K K)
    (t : Finset {z : S // z ≠ 0}) :
    ∃ C : Set (S → ℝ), C ⊆ K ∧ C.Nonempty ∧ IsCompact C ∧ Convex ℝ C ∧
      (∀ z : S, z ≠ 0 → MapsTo (normalizedTranslate z) C C) ∧
      ∀ f ∈ C, ∀ z ∈ t, ∀ x, f (z.val * x) = f z.val * f x := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate

  19. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_multiplicative_of_invariant_states line 155

    Source documentation

    A compact convex normalized state space invariant under multiplication translates contains a multiplicative state. Frozen eigenvalue slices preserve convexity at each finite fixed-point step.

    theorem exists_multiplicative_of_invariant_states {K : Set (S → ℝ)}
    (hKcompact : IsCompact K) (hKconvex : Convex ℝ K) (hKne : K.Nonempty)
    (hKnorm : ∀ f ∈ K, f 1 = 1) (hKzero : ∀ f ∈ K, f 0 = 0)
    (hKnonzero : ∀ f ∈ K, ∀ z : S, z ≠ 0 → f z ≠ 0)
    (hKmap : ∀ z : S, z ≠ 0 → MapsTo (normalizedTranslate z) K K) :
    ∃ f ∈ K, ∀ x y, f (x * y) = f x * f y := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate

  20. theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates_exists_multiplicative line 188

    Source documentation

    Appendix A.2 for a ranked restriction semiring: once the preliminary normalized state set is nonempty, it contains a multiplicative state.

    theorem normalizedStates_exists_multiplicative [Preorder S]
    (R : S → ℕ) (d : S) (k : ℝ)
    (hunit : ∀ z : S, z ≠ 0 → 1 ≤ z)
    (hmulmono : ∀ z x y : S, x ≤ y → z * x ≤ z * y)
    (hdom : ∀ z x : S, z * x ≤ (R x : S) * z)
    (hne : (normalizedStates (fun x => (R x : ℝ)) d k).Nonempty) :
    ∃ f ∈ normalizedStates (fun x => (R x : ℝ)) d k,
      ∀ x y, f (x * y) = f x * f y := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates

  21. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_monotone_semiringHom_of_normalizedStates line 207

    Source documentation

    The multiplicative state as a normalized monotone semiring homomorphism, with the original rank bounds and detector inequality preserved.

    theorem exists_monotone_semiringHom_of_normalizedStates [Preorder S]
    (R : S → ℕ) (d : S) (k : ℝ)
    (hunit : ∀ z : S, z ≠ 0 → 1 ≤ z)
    (hmulmono : ∀ z x y : S, x ≤ y → z * x ≤ z * y)
    (hdom : ∀ z x : S, z * x ≤ (R x : S) * z)
    (hne : (normalizedStates (fun x => (R x : ℝ)) d k).Nonempty) :
    ∃ χ : S →+* ℝ, Monotone χ ∧ (∀ x, 0 ≤ χ x ∧ χ x ≤ R x) ∧ k ≤ χ d := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates