OAI/Combinatorics/ContingencyTables/Dense/GridMass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Continuous mass and weighted grid cuts

Unit bins have disjoint interiors and exact volume one. Their continuous mass is compared with the discrete weights, and the finite shell cover converts interpolation gain into a weighted cut-face sum.

  1. def OAI.ContingencyTables.GridBoundary.binSet line 20
  2. def OAI.ContingencyTables.GridBoundary.ambientBox line 23
  3. abbrev OAI.ContingencyTables.GridBoundary.Selected line 26
  4. instance OAI.ContingencyTables.GridBoundary.(instance at line 29) line 29
  5. theorem OAI.ContingencyTables.GridBoundary.binSet_pi line 32
  6. theorem OAI.ContingencyTables.GridBoundary.binSet_measurable line 37
  7. theorem OAI.ContingencyTables.GridBoundary.binSet_volume line 41
  8. theorem OAI.ContingencyTables.GridBoundary.binSet_disjoint line 45
  9. theorem OAI.ContingencyTables.GridBoundary.binSet_subset_ambient line 56
  10. theorem OAI.ContingencyTables.GridBoundary.selectedBins_finiteBox line 61
  11. theorem OAI.ContingencyTables.GridBoundary.cube_finiteBox line 74
  12. theorem OAI.ContingencyTables.GridBoundary.selectedBins_closure line 79
  13. theorem OAI.ContingencyTables.GridBoundary.cube_closure line 85
  14. theorem OAI.ContingencyTables.GridBoundary.selectedBins_integral line 90
  15. theorem OAI.ContingencyTables.GridBoundary.selectedBins_mass_lower line 110

    Source documentation

    The selected side has at least one quarter of its own discrete mass; it need not be the smaller side for the discrete weights.

    theorem selectedBins_mass_lower (P : (Fin q → ℤ) → Prop) (ρ : (Fin q → ℝ) → ℝ)
    (w : Grid (I := Fin q) K → ℝ) (hi : IntegrableOn ρ (ambientBox q K))
…

    Mentions: OAI.ContingencyTables.GridBoundary.Grid, OAI.ContingencyTables.GridBoundary.ambientBox

  16. theorem OAI.ContingencyTables.GridBoundary.edgeTube_mass_upper line 122