OAI/Combinatorics/ContingencyTables/Dense/AffineRegion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Inner and relaxed affine feasibility regions

The strict feasible point yields the two homothetic inclusions used in the dense rejection proof. Volume scaling follows from the Lebesgue/Haar change-of-variables theorem.

  1. def OAI.ContingencyTables.AffinePenalty.region line 23
  2. theorem OAI.ContingencyTables.AffinePenalty.inner_region_map line 26
  3. theorem OAI.ContingencyTables.AffinePenalty.relaxed_region_pullback line 37
  4. theorem OAI.ContingencyTables.AffinePenalty.relaxed_region_subset_expansion line 56
  5. theorem OAI.ContingencyTables.AffinePenalty.volume_image_translate line 69
  6. theorem OAI.ContingencyTables.AffinePenalty.volume_homothety line 80
  7. theorem OAI.ContingencyTables.AffinePenalty.relaxed_region_volume line 92