PublishedInputs.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The published analytic input for result 200

Prékopa, On logarithmic concave measures and functions, Acta Sci. Math. (Szeged) 34 (1973), 335–343, Theorem 3, equation (2.3), with two source functions. Source: https://acta.bibl.u-szeged.hu/14411/1/math_034_335-343.pdf The one-dimensional input is Leindler (1972), On a certain converse of Hölder's inequality II, 217–223, as identified in Prékopa's §2.

The finite-box specialization allows positive continuous functions on a common compact coordinate box and finite unions of open boxes.

abbrev OAI.ContingencyTables.PublishedInputs.Point line 25
def OAI.ContingencyTables.PublishedInputs.IsFiniteBoxUnion line 29
Source documentation
The bounded finite unions of open coordinate boxes used by the bin conductance argument. Empty unions and empty coordinate boxes are allowed.
```
def IsFiniteBoxUnion {q : ℕ} (S : Set (Point q)) : Prop :=
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.Point
def OAI.ContingencyTables.PublishedInputs.interpolate line 34
Source documentation
The weighted Minkowski interpolation with the manuscript convention.
```
def interpolate {q : ℕ} (t : ℝ) (S T : Set (Point q)) : Set (Point q) :=
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.Point
def OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler line 40
Source documentation
Precisely the previously published finite-box integral interpolation input. The functions need only be positive and continuous on the common compact coordinate box; all integrals are Lebesgue integrals.
```
def FiniteBoxPrekopaLeindler (q : ℕ) : Prop :=
…
```
def OAI.ContingencyTables.PublishedInputs.LogConcaveOn line 61
Source documentation
Log-concavity is needed only on the common ambient box.
```
def LogConcaveOn {q : ℕ} (ρ : Point q → ℝ) (K : Set (Point q)) : Prop :=
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.Point

theorem OAI.ContingencyTables.PublishedInputs.density_interpolation line 67

Source documentation

Specialization of the published input to the one log-concave density used for bin conductance. The geometric hypotheses specify the common ambient box.

theorem density_interpolation {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)
    (hM : IsFiniteBoxUnion (interpolate t S T))
    (hSc : closure S ⊆ Set.Icc lower upper)
    (hTc : closure T ⊆ Set.Icc lower upper)
    (hMc : closure (interpolate t S 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)) :
    (∫ x in S, ρ x) ^ (1 - t) * (∫ y in T, ρ y) ^ t ≤
…

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