SignRandomization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform sign randomization of a fixed solution

The sign mask is uniform among all indexed subsets. Toggling a fixed solution is a bijection on that exact finite space, so it is also uniform. This is the distributional step preceding the representation balance event.

def OAI.LowSpaceSubsetSum.toggleEquiv line 20

theorem OAI.LowSpaceSubsetSum.toggle_event_card line 27

Source documentation

Exact event counting for a uniformly chosen sign mask.

theorem toggle_event_card (S : Finset ι) (A : Finset (Finset ι)) :
    (Finset.univ.filter fun F : Finset ι => S ∆ F ∈ A).card = A.card := by
…

theorem OAI.LowSpaceSubsetSum.toggle_event_probability line 47

Source documentation

The equality is of probabilities, not merely of supports.

theorem toggle_event_probability (S : Finset ι) (A : Finset (Finset ι)) :
    ((Finset.univ.filter fun F : Finset ι => S ∆ F ∈ A).card : ℝ) /
      (2 : ℝ) ^ Fintype.card ι = A.card / (2 : ℝ) ^ Fintype.card ι := by
…