OAI/Combinatorics/ContingencyTables/Dense/FiniteBoxPrekopa.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Discharging the finite-box Prékopa–Leindler input

The finite-function-space Prékopa–Leindler inequality applies to the nonnegative indicators of the three box unions. Compact-box continuity supplies all measurability and integrability obligations without assumptions outside the common box.

  1. theorem OAI.ContingencyTables.PublishedInputs.integral_interpolation line 19
  2. theorem OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion.isOpen line 40

    Distinct definitions of this name: OAI/Combinatorics/ContingencyTables/Transport/BoxGeometry.lean:105 (same statement text; different proof or body). Qualify references as OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion.isOpen@path.

  3. theorem OAI.ContingencyTables.PublishedInputs.box_indicator line 52
  4. theorem OAI.ContingencyTables.PublishedInputs.finiteBoxPrekopaLeindler line 71

    Source documentation

    The exact published analytic hypothesis required by both manuscripts.

    theorem finiteBoxPrekopaLeindler (q : ℕ) : FiniteBoxPrekopaLeindler q := by
…

    Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler