OAI/Combinatorics/ContingencyTables/Transport/IntegerChildLogConcavity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Conditional child masses have no internal valley

The actual two-coordinate removal form gives the local log-concavity inequality. The endpoint-minimum property passes to the hard-zero limit.

  1. def OAI.ContingencyTables.IntegerWeightedTransport.childProfile line 17
  2. lemma OAI.ContingencyTables.IntegerWeightedTransport.bool_diagonal_product line 19
  3. lemma OAI.ContingencyTables.IntegerWeightedTransport.childProfile_inBox line 30
  4. lemma OAI.ContingencyTables.IntegerWeightedTransport.childProfile_total line 37
  5. theorem OAI.ContingencyTables.IntegerWeightedTransport.child_logConcave line 41
  6. theorem OAI.ContingencyTables.IntegerWeightedTransport.child_minimum line 85
  7. theorem OAI.ContingencyTables.IntegerWeightedTransport.child_minimum_limit line 99

    Source documentation

    Every mass between two positive hard children is at least the smaller endpoint mass, including when other children have zero weight.

    theorem child_minimum_limit {K : Type*} {l : Filter K} [l.NeBot]
    (F : K → (Bool → ℕ) → ℝ) (f : (Bool → ℕ) → ℝ) (U : ℕ)
    (hlim : ∀ z, Tendsto (fun t => F t z) l (nhds (f z)))
    (hsoft : ∀ᶠ t in l, PositiveSlice (F t) (fun _ => U) U ∧
      RemovalSlice (F t) (fun _ => U) U)
    (a j b : ℕ) (haj : a ≤ j) (hjb : j ≤ b) (hbU : b ≤ U) :
    min (f (childProfile U a)) (f (childProfile U b)) ≤ f (childProfile U j) := by
…

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.childProfile