ShortcodeFiberSampling.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Exact finite output-fiber sampling identities. These connect the weighted kernel extraction to uniform sampling of a matrix in the actual output fiber.

theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.matrixKernel_average line 16
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiberMass_eq_card line 27
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiberMass_pos_iff line 40
def OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiberFactorRetention line 48
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiberFlow_eq line 52
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiber_retention_eq_factor_average line 68
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiberFactorRetention_zero_left line 90
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiberFactorRetention_zero_right line 101
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.exists_output_fiber_factor_retention line 114
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.MaxCutGames.Inverse.ShortcodeFromGrassmann.matrixFiber, OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.fiberFactorRetention

theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.uniform_pair_mixture line 132

Source documentation

Exact decomposition of a uniform two-factor law with a self-loop on either zero factor. No nonemptiness is required of the nonzero subtypes.

theorem uniform_pair_mixture {A B : Type*} [Fintype A] [Fintype B]
    [Zero A] [Zero B] (h : A → B → ℝ)
    (hleft : ∀ b, h 0 b = 1) (hright : ∀ a, h a 0 = 1) :
    (𝔼 a, 𝔼 b, h a b) =
      (Fintype.card A : ℝ)⁻¹ + (Fintype.card B : ℝ)⁻¹ -
        (Fintype.card A : ℝ)⁻¹ * (Fintype.card B : ℝ)⁻¹ +
      (1 - ((Fintype.card A : ℝ)⁻¹ + (Fintype.card B : ℝ)⁻¹ -
        (Fintype.card A : ℝ)⁻¹ * (Fintype.card B : ℝ)⁻¹)) *
        (𝔼 p : {a : A // a ≠ 0} × {b : B // b ≠ 0}, h p.1.val p.2.val) := by
…

theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.vector_card_real_inline_ShortcodeFiberConditioning line 204
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.binary_zero_mass_nonneg_inline_ShortcodeFiberConditioning line 208

theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.conditioned_output_fiber line 222

Source documentation

The actual equality test has a nonempty output fiber retaining at least η/2 after both factors are conditioned to be nonzero. The displayed order samples a uniform matrix in that fiber first, as required by the Grassmann neighbor correspondence.

theorem conditioned_output_fiber {ell m : ℕ}
    (f : Mat ell m → Vector ell) {η : ℝ} (hη : 0 < η) (hη1 : η < 1)
    (hzero : ((2 : ℝ) ^ ell)⁻¹ + ((2 : ℝ) ^ m)⁻¹ -
      ((2 : ℝ) ^ (ell + m))⁻¹ ≤ η / 2)
    (haccept : η ≤ equalityAcceptance f) :
    ∃ y, (matrixFiber f y).Nonempty ∧
      η / 2 ≤ (matrixFiber f y).expect (fun M =>
        𝔼 p : {a : Vector ell // a ≠ 0} × {l : Vector m // l ≠ 0},
          if f (M + rankOne p.1.val p.2.val) = y then (1 : ℝ) else 0) := by
…

Mentions: OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.matrixFiber

theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.chartFiberRetention line 258
Source documentation
The finite sampling bridge has no expansion or inverse premise.
```
theorem chartFiberRetention : ChartFiberRetention := by
…
```
Mentions: OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.ChartFiberRetention
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.inversePrinciple_of_expansion line 272
Source documentation
Conditional Grassmann-to-matrix implication, preserving all quantifiers and the affine target. KMS expansion is the sole remaining displayed premise.
```
theorem inversePrinciple_of_expansion (hKMS : KMS.ExpansionPrinciple) :
    Shortcode.InversePrinciple :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.ExpansionPrinciple, OAI.MaxCutGames.Inverse.Shortcode.InversePrinciple
theorem OAI.MaxCutGames.Inverse.ShortcodeTheorem.inversePrinciple line 288
Source documentation
Full-factor sampling includes zero. The conclusion retains an affine intercept and applies to arbitrary matrix labelings without a folding premise.
```
theorem inversePrinciple : Shortcode.InversePrinciple :=
…
```
Mentions: OAI.MaxCutGames.Inverse.Shortcode.InversePrinciple