BoxGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite-box geometry for the conditional conductance argument

Finite unions of grid boxes remain finite unions of boxes under weighted Minkowski interpolation, giving the domain hypothesis of Prékopa–Leindler.

theorem OAI.ContingencyTables.PublishedInputs.scalar_box_interpolation line 21
theorem OAI.ContingencyTables.PublishedInputs.finite_box_union_of_fintype line 45
theorem OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion.interpolate line 60
Source documentation
Interpolation preserves exactly the finite-box class appearing in Prékopa's published integral inequality.
```
theorem IsFiniteBoxUnion.interpolate {q : ℕ} {S T : Set (Point q)}
    (hS : IsFiniteBoxUnion S) (hT : IsFiniteBoxUnion T)
    (t : ℝ) (ht : 0 < t) (ht1 : t < 1) :
    IsFiniteBoxUnion (interpolate t S T) := by
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.Point, OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion
theorem OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion.isOpen line 105
Distinct definitions of this name: OAI/Combinatorics/ContingencyTables/Dense/FiniteBoxPrekopa.lean:40 (same statement text; different proof or body). Qualify references as OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion.isOpen@path.
theorem OAI.ContingencyTables.PublishedInputs.interpolation_closure_in_box line 120
theorem OAI.ContingencyTables.PublishedInputs.weighted_geometric_doubling line 129

theorem OAI.ContingencyTables.PublishedInputs.interpolation_shell_gain line 150

Source documentation

The interpolation shell gains the mass used in the grid-cut proof. This conditional result depends only on the precisely identified published integral inequality; finite-box closure and integrability are proved here.

theorem interpolation_shell_gain {q : ℕ} (hPL : FiniteBoxPrekopaLeindler q)
    (t : ℝ) (ht : 0 < t) (ht1 : t < 1)
    (lower upper : Point q) (S T : Set (Point q)) (ρ : Point q → ℝ)
    (hS : IsFiniteBoxUnion S) (hT : IsFiniteBoxUnion T)
    (hSc : closure S ⊆ Set.Icc lower upper)
    (hTc : closure T ⊆ Set.Icc lower upper)
    (hρ : ContinuousOn ρ (Set.Icc lower upper))
    (hpos : ∀ x ∈ Set.Icc lower upper, 0 < ρ x)
    (hlc : LogConcaveOn ρ (Set.Icc lower upper))
    (hsub : S ⊆ interpolate t S T)
    (hSmass : 0 < ∫ x in S, ρ x)
    (hTmass : 2 * (∫ x in S, ρ x) ≤ ∫ x in T, ρ x) :
…

Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.Point, OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion, OAI.ContingencyTables.PublishedInputs.LogConcaveOn, OAI.ContingencyTables.PublishedInputs.interpolate