EqualityFiber.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite equality-fiber extraction for the Grassmann-to-matrix route.

These elementary results do not assume a shortcode inverse theorem. They separate the equality test, the retention of a nonempty output fiber, and the subsequent removal of zero perturbation factors. The dimension-uniform Grassmann expansion theorem remains a separate mathematical obligation.

def OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberMass line 26
def OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberFlow line 30
def OAI.UniqueGamesTheorem.Inverse.EqualityFiber.equalityAcceptance line 34
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.sum_fiberMass line 38
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberMass_nonneg line 46
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberFlow_nonneg line 56
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberFlow_le_mass line 69
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.sum_sameFiber_indicator line 87
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.sum_fiberFlow line 100

theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.exists_positive_mass_le_flow line 115

Source documentation

A probability-weighted average at least η contains a positive-weight fiber whose unnormalized flow is at least η times its mass.

theorem exists_positive_mass_le_flow (mass flow : Y → ℝ)
    (hmass : IsProbability mass) (_hflow : ∀ y, 0 ≤ flow y)
    (hzero : ∀ y, mass y = 0 → flow y = 0)
    {η : ℝ} (haccept : η ≤ ∑ y, flow y) :
    ∃ y, 0 < mass y ∧ η * mass y ≤ flow y := by
…

theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.exists_fiber_retention line 145
Source documentation
Equality acceptance supplies a nonempty output fiber with the claimed retention. The kernel is the actual sampling kernel; no conditioned sampling law is silently substituted.
```
theorem exists_fiber_retention (p : X → ℝ) (k : X → X → ℝ)
    (hp : IsProbability p) (hk : ∀ x, IsProbability (k x))
    (f : X → Y) {η : ℝ} (haccept : η ≤ equalityAcceptance p k f) :
    ∃ y, 0 < fiberMass p f y ∧ η ≤ fiberFlow p k f y / fiberMass p f y := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.EqualityFiber.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberMass, OAI.UniqueGamesTheorem.Inverse.EqualityFiber.fiberFlow
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.nonzero_retention_ge_half line 162
Source documentation
Removing a self-loop mass p₀ ≤ η/2 leaves retention at least η/2. This is the precise algebra needed when one or both rank-one factors may be zero in the unconditioned test.
```
theorem nonzero_retention_ge_half {η p₀ R : ℝ}
    (hη : 0 < η) (hη1 : η < 1) (hp₀ : 0 ≤ p₀) (hp₀η : p₀ ≤ η / 2)
    (haccept : η ≤ p₀ + (1 - p₀) * R) : η / 2 ≤ R := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.EqualityFiber.chart_retention_ge_quarter line 170