OAI/Combinatorics/ContingencyTables/Transport/IntegerFutureSquare.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.IntegerWeightedTransport.sum_range_shift line 17
2. lemma OAI.ContingencyTables.IntegerWeightedTransport.sum_range_truncate line 30
3. lemma OAI.ContingencyTables.IntegerWeightedTransport.sum_middle_shift line 43
4. lemma OAI.ContingencyTables.IntegerWeightedTransport.future_aa line 57
5. lemma OAI.ContingencyTables.IntegerWeightedTransport.future_bb line 66
6. lemma OAI.ContingencyTables.IntegerWeightedTransport.future_ab line 78
7. theorem OAI.ContingencyTables.IntegerWeightedTransport.future_new_square line 93

   Source documentation

   The exact new--new part of the future correction: two diagonal removals and the mixed removal of the same integer pair form a square.

   theorem future_new_square
       (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (n : ℕ) (g : ℕ → ℝ) :
       (∑ j ∈ Finset.range (n+3),
         (pairMatrix F (n+2) z j (.inr false) (.inr false) * g j ^ 2 -
         2 * pairMatrix F (n+2) z j (.inr false) (.inr true) * g j * g (j+1) +
         pairMatrix F (n+2) z j (.inr true) (.inr true) * g (j+1) ^ 2)) =
         ∑ k ∈ Finset.range (n+1), F (profile z k (n-k)) * (g (k+2)-g (k+1)) ^ 2 := by
   …

8. theorem OAI.ContingencyTables.IntegerWeightedTransport.future_new_nonnegative line 140

   Source documentation

   Every kernel entry has the same complete configuration; positivity alone makes the future correction nonnegative.

   theorem future_new_nonnegative
       (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (n : ℕ) (g : ℕ → ℝ)
       (hF : ∀ p, 0 ≤ F p) :
       0 ≤ ∑ j ∈ Finset.range (n+3),
         (pairMatrix F (n+2) z j (.inr false) (.inr false) * g j ^ 2 -
         2 * pairMatrix F (n+2) z j (.inr false) (.inr true) * g j * g (j+1) +
         pairMatrix F (n+2) z j (.inr true) (.inr true) * g (j+1) ^ 2) := by
   …

9. theorem OAI.ContingencyTables.IntegerWeightedTransport.future_mixed_cancel line 153

   Source documentation

   The two mixed old--new sums telescope, including both invalid endpoint removals.

   theorem future_mixed_cancel
       (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (M : ℕ)
       (h : I → ℝ) (g : ℕ → ℝ) :
       (∑ j ∈ Finset.range (M+1),
         ((pairMatrix F M z j).toBilin' (old h) (Pi.single (.inr false) 1) * g j -
         (pairMatrix F M z j).toBilin' (old h) (Pi.single (.inr true) 1) * g (j+1))) = 0 := by
   …

10. theorem OAI.ContingencyTables.IntegerWeightedTransport.future_old_sum line 171

    Source documentation

    Old--old entries partition the parent's balanced marginal exactly.

    theorem future_old_sum
        (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (M : ℕ) (h : I → ℝ) :
        (∑ j ∈ Finset.range (M+1), (pairMatrix F M z j).toBilin' (old h) (old h)) =
          (integerRemovalMatrix (marginal F M) z).toBilin' h h := by
    …

11. def OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients line 179
12. lemma OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients_inl line 184
13. lemma OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients_a line 189
14. lemma OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients_b line 194
15. lemma OAI.ContingencyTables.IntegerWeightedTransport.extended_quadratic line 198
16. theorem OAI.ContingencyTables.IntegerWeightedTransport.future_square_identity line 219

    Source documentation

    Equation future-square of the first manuscript for actual integer removal matrices. The parent is the balanced raw marginal.

    theorem future_square_identity
        (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (n : ℕ)
        (h : I → ℝ) (g : ℕ → ℝ) :
        (∑ j ∈ Finset.range (n+3),
          (pairMatrix F (n+2) z j).toBilin'
            (extendCoefficients h (g j) (g (j+1))) (extendCoefficients h (g j) (g (j+1)))) -
          (integerRemovalMatrix (marginal F (n+2)) z).toBilin' h h =
        ∑ k ∈ Finset.range (n+1), F (profile z k (n-k)) * (g (k+2)-g (k+1))^2 := by
    …

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients

17. theorem OAI.ContingencyTables.IntegerWeightedTransport.future_form_monotone line 236

    Source documentation

    Processing an ordinary integer pair can only increase a future form. No signature assertion about the weighted future kernel is required.

    theorem future_form_monotone
        (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (n : ℕ)
        (h : I → ℝ) (g : ℕ → ℝ) (hF : ∀ p, 0 ≤ F p) :
        (integerRemovalMatrix (marginal F (n+2)) z).toBilin' h h ≤
          ∑ j ∈ Finset.range (n+3), (pairMatrix F (n+2) z j).toBilin'
            (extendCoefficients h (g j) (g (j+1))) (extendCoefficients h (g j) (g (j+1))) := by
    …

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients