OAI/Computability/UniqueGames/Inverse/ShortcodeFiberLemmas.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The actual uniform matrix test supplies a positive-mass output fiber with large retention. The transition kernel averages independent full vectors, including zero.

  1. def OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixWeight line 21
  2. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixWeight_probability line 24
  3. def OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixKernel line 33
  4. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixKernel_nonneg line 37
  5. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixKernel_probability line 45
  6. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixKernel_equality line 58
  7. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance_eq_kernel line 71
  8. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.exists_output_fiber line 92

    Source documentation

    Positive-mass fibers, with their actual transition flow, are obtained from the full uniform factor law. This is the first step before conditioning both factors to be nonzero and passing to Grassmann neighbors.

    theorem exists_output_fiber {ell m : ℕ} (f : Mat ell m → Vector ell)
    {η : ℝ} (haccept : η ≤ equalityAcceptance f) :
    ∃ y : Vector ell, 0 < EqualityFiber.fiberMass matrixWeight f y ∧
      η ≤ EqualityFiber.fiberFlow matrixWeight matrixKernel f y /
        EqualityFiber.fiberMass matrixWeight f y := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector, OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberMass, OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixWeight, OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberFlow, OAI.UniqueGamesTheorem.Inverse.Shortcode.matrixKernel

  9. def OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.matrixFiber line 114
  10. def OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.liftedFiber line 117
  11. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.liftedFiber_subset_chart line 120
  12. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.matrixVertex_mem_liftedFiber line 127
  13. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.image_slice_points line 141

    Source documentation

    The slice and the interval intersected with the chart correspond exactly. The hypothesis states equality of the actual membership predicates.

    theorem image_slice_points {ell m : ℕ} (S : Slice ell m)
    (I : Finset (KMS.Vertex (ell + m) ell))
    (hS : ∀ M, S.Contains M ↔ matrixVertex M ∈ I) :
    S.points.image matrixVertex = I ∩ matrixChart ell m := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex

  14. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.image_slice_fiber line 157
  15. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.constantAgreement_eq_chart_density line 181

    Source documentation

    Uniform agreement on a slice is the actual Grassmann fiber density in the chart-intersected interval. Empty sets are allowed on both sides of this identity, with the standard zero-denominator convention.

    theorem constantAgreement_eq_chart_density {ell m : ℕ} (S : Slice ell m)
    (I : Finset (KMS.Vertex (ell + m) ell))
    (hS : ∀ M, S.Contains M ↔ matrixVertex M ∈ I)
    (f : Mat ell m → Vector ell) (y : Vector ell) :
    S.constantAgreement f y =
      KMS.relativeDensity (liftedFiber f y) (I ∩ matrixChart ell m) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.liftedFiber

  16. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.hasAffineSlice_of_dense_interval line 192
  17. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.matrixKernel_average line 227
  18. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiberMass_eq_card line 238
  19. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiberMass_pos_iff line 251
  20. def OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiberFactorRetention line 259
  21. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiberFlow_eq line 263
  22. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiber_retention_eq_factor_average line 279
  23. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiberFactorRetention_zero_left line 301
  24. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiberFactorRetention_zero_right line 312
  25. theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.exists_output_fiber_factor_retention line 325

    Source documentation

    A nonempty actual output fiber whose retention under the full factor law is at least the original equality acceptance threshold.

    theorem exists_output_fiber_factor_retention {ell m : ℕ}
    (f : Mat ell m → Vector ell) {η : ℝ} (haccept : η ≤ equalityAcceptance f) :
    ∃ y, (matrixFiber f y).Nonempty ∧ η ≤ 𝔼 a, 𝔼 l, fiberFactorRetention f y a l := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.matrixFiber, OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.fiberFactorRetention