AffineWitnessFiniteDensity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite indicator expectations as conditional cardinality ratios

These identities use the complete finite sample set in the denominator. They also cover the empty set, for which both the expectation and the ratio are zero. The equivalence variant transfers both the event and the sample space, so no conditioning factor is lost when changing representations of a slice.

theorem OAI.MaxCutGames.Inverse.card_finset_subtype_eq_filter_card line 23
Source documentation
Filtering a finite sample set counts the same objects as first restricting to the sample set and then imposing the event predicate.
```
theorem card_finset_subtype_eq_filter_card (s : Finset X)
    (p : X → Prop) [DecidablePred p] :
    Nat.card {x : s // p x.val} = (s.filter p).card := by
…
```

theorem OAI.MaxCutGames.Inverse.finset_expect_indicator_eq_card_ratio line 39

Source documentation

An indicator's expectation on a finite set is its agreement count divided by the cardinality of that same finite set.

theorem finset_expect_indicator_eq_card_ratio (s : Finset X)
    (p : X → Prop) [DecidablePred p] :
    s.expect (fun x => if p x then (1 : ℝ) else 0) =
      (Nat.card {x : s // p x.val} : ℝ) / (Nat.card s : ℝ) := by
…

theorem OAI.MaxCutGames.Inverse.nat_card_subtype_equiv line 48
Source documentation
A bijection preserving the event preserves its count. No choice of a Fintype enumeration is involved in this identity.
```
theorem nat_card_subtype_equiv (e : X ≃ Y) (p : X → Prop) (q : Y → Prop)
    (h : ∀ x, p x ↔ q (e x)) :
    Nat.card {x : X // p x} = Nat.card {y : Y // q y} :=
…
```

theorem OAI.MaxCutGames.Inverse.finset_expect_indicator_eq_card_ratio_of_equiv line 55

Source documentation

Transfer the indicator expectation through an equivalence of the complete finite sample space, including the denominator of the conditional law.

theorem finset_expect_indicator_eq_card_ratio_of_equiv (s : Finset X)
    (p : X → Prop) [DecidablePred p] (e : ↥s ≃ Y) (q : Y → Prop)
    (h : ∀ x : s, p x.val ↔ q (e x)) :
    s.expect (fun x => if p x then (1 : ℝ) else 0) =
      (Nat.card {y : Y // q y} : ℝ) / (Nat.card Y : ℝ) := by
…

def OAI.MaxCutGames.Inverse.Shortcode.functionalRow line 77
Source documentation
The coordinate row of a binary linear functional.
```
def functionalRow (e : Vector m →ₗ[F2] F2) : Vector m :=
…
```
Mentions: OAI.MaxCutGames.Inverse.Shortcode.Vector, OAI.MaxCutGames.Inverse.Shortcode.F2
theorem OAI.MaxCutGames.Inverse.Shortcode.toMatrix_shift line 80

theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.affineAgreement_eq_linear_ratio line 94

Source documentation

Exact density identity on the complete nonempty affine slice, with no lost conditioning factor in the change from matrices to linear maps.

theorem affineAgreement_eq_linear_ratio (S : Slice ell m)
    (M₀ : Mat ell m) (hM₀ : S.Contains M₀)
    (f : Mat ell m → Vector ell) (z : Vector m) (u : Vector ell) :
    S.affineAgreement f z u =
      (Nat.card {N : AffineWitness.Slice S.rowMap S.columnSpan (Matrix.toLin' M₀) //
        f (LinearMap.toMatrix' N.val) = N.val z + u} : ℝ) /
      (Nat.card (AffineWitness.Slice S.rowMap S.columnSpan (Matrix.toLin' M₀)) : ℝ) := by
…

Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat, OAI.MaxCutGames.Inverse.Shortcode.Vector, OAI.MaxCutGames.Inverse.AffineWitness.Slice

theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.first_bit_normalization line 113

Source documentation

First-bit normalization for the exact selected shortcode slice. The original affine agreement is preserved, not merely bounded below.

theorem first_bit_normalization (S : Slice ell m)
    (M₀ : Mat ell m) (hM₀ : S.Contains M₀)
    (e : Vector m →ₗ[F2] F2)
    (f : Mat ell m → Vector ell) (z : Vector m) (u : Vector ell)
    (hfold : ∀ (h : S.rowMap.ker) M,
      f (M + rankOne h (functionalRow e)) = f M + h)
    (α : ℝ) (hα : 0 < α) (hgood : α / 2 ≤ S.affineAgreement f z u)
    (hsmall : 1 / (2 : ℝ) ^ (ell - S.rows) < α / 8) :
    ∃ z' : Vector m, ∃ u' : Vector ell, e z' = 1 ∧
      S.affineAgreement f z' u' = S.affineAgreement f z u ∧
      ∀ M, S.Contains M → evaluate M z' + u' = evaluate M z + u := by
…

Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat, OAI.MaxCutGames.Inverse.Shortcode.Vector, OAI.MaxCutGames.Inverse.Shortcode.F2, OAI.MaxCutGames.Inverse.Shortcode.rankOne, OAI.MaxCutGames.Inverse.Shortcode.functionalRow, OAI.MaxCutGames.Inverse.Shortcode.evaluate