OAI/Combinatorics/ContingencyTables/Transport/PositiveSequenceInterpolation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.decreasing_increments_average line 16
2. theorem OAI.ContingencyTables.discrete_secant line 33

   Source documentation

   A finite sequence with decreasing adjacent increments lies above each secant joining its first point to a later point.

   theorem discrete_secant (g : ℕ → ℝ) (N : ℕ)
       (hc : ∀ k, k+2 ≤ N → g k+g (k+2) ≤ 2*g (k+1))
       (n : ℕ) (hn : n ≤ N) (k : ℕ) (hk : k ≤ n) :
       (k:ℝ)*(g n-g 0) ≤ (n:ℝ)*(g k-g 0) := by
   …

3. theorem OAI.ContingencyTables.positive_sequence_log_secant line 60

   Source documentation

   Adjacent log-concavity gives the exact finite logarithmic secant inequality used for each positive tree-coordinate marginal.

   theorem positive_sequence_log_secant (a : ℕ → ℝ) (N : ℕ)
       (hp : ∀ k, k ≤ N → 0 < a k)
       (hc : ∀ k, k+2 ≤ N → a k*a (k+2) ≤ (a (k+1))^2)
       (k : ℕ) (hk : k ≤ N) :
       (k:ℝ)*(Real.log (a N)-Real.log (a 0)) ≤
         (N:ℝ)*(Real.log (a k)-Real.log (a 0)) := by
   …

4. theorem OAI.ContingencyTables.positive_sequence_half_window line 78

   Source documentation

   A positive log-concave sequence whose far endpoint has mass at least one and whose first mass is at most 2^K loses at most a factor two over the first N/K integer positions.

   theorem positive_sequence_half_window (a : ℕ → ℝ) (N K : ℕ)
       (hK : 1 ≤ K) (hN : 0 < N)
       (hp : ∀ k, k ≤ N → 0 < a k)
       (hc : ∀ k, k+2 ≤ N → a k*a (k+2) ≤ (a (k+1))^2)
       (hend : 1 ≤ a N) (hfirst : a 0 ≤ (2:ℝ)^K)
       (r : ℕ) (hr : r*K ≤ N) : a 0/2 ≤ a r := by
   …

5. theorem OAI.ContingencyTables.half_window_mass_bound line 105

   Source documentation

   A half-height interpolation window contains enough distinct integer positions to give the source's normalized exterior point-mass bound.

   theorem half_window_mass_bound (a : ℕ → ℝ) (U k N K b : ℕ)
       (hK : 0 < K) (hb : 0 < b) (hbN : b ≤ N) (hkN : k+N ≤ U)
       (ha : ∀ j,j ≤ U → 0 ≤ a j)
       (hC : 0 < ∑ j ∈ Finset.range (U+1),a j)
       (hwindow : ∀ r,r*K ≤ N → a k/2 ≤ a (k+r)) :
       a k/(∑ j ∈ Finset.range (U+1),a j) ≤ (2*K:ℝ)/b := by
   …