IntegerFutureKernel.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The weighted future-slot kernel

Weights a(M-a) are used inside the finite box 0≤a≤M. The common nonnegative kernel identifies the integer transport's future correction matrix.

def OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture line 20
lemma OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture_nonnegative line 24
theorem OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture_matrix line 35
Source documentation
Weighted future matrices are the old block of the literal common kernel. This is an equality, with no one-positive-direction hypothesis.
```
theorem weightedFuture_matrix (F : ((I ⊕ Bool) → ℕ) → ℝ) (M : ℕ) (z : I → ℕ) :
    integerRemovalMatrix (weightedFuture F M) z =
      ∑ a ∈ Finset.range (M+1), ((a:ℝ)*((M:ℝ)-a)) •
        (pairMatrix F M z a).submatrix Sum.inl Sum.inl := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture

theorem OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture_form line 45

Source documentation

The scalar correction Q_t is exactly the weighted two-old-hole sum.

theorem weightedFuture_form (F : ((I ⊕ Bool) → ℕ) → ℝ) (M : ℕ)
    (z : I → ℕ) (h : I → ℝ) :
    (integerRemovalMatrix (weightedFuture F M) z).toBilin' h h =
      ∑ a ∈ Finset.range (M+1), (a:ℝ)*((M:ℝ)-a)*
        (pairMatrix F M z a).toBilin' (old h) (old h) := by
…

Mentions: OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture

theorem OAI.ContingencyTables.IntegerWeightedTransport.weighted_future_monotone line 58

Source documentation

Applying the square identity to the manuscript's weighted future kernel proves monotonicity for that kernel itself.

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

Mentions: OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture, OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients

def OAI.ContingencyTables.IntegerWeightedTransport.swapPairs line 68
Source documentation
Exchange the current and future pairs, leaving all old coordinates fixed. This makes the common summation domain explicit.
```
def swapPairs : ((I ⊕ Bool) ⊕ Bool) ≃ ((I ⊕ Bool) ⊕ Bool) where
…
```
lemma OAI.ContingencyTables.IntegerWeightedTransport.profile_swap line 81
theorem OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture_marginal_commute line 90
Source documentation
The weighted future sum and the current balanced sum commute on one fixed set of complete configurations.
```
theorem weightedFuture_marginal_commute
    (F : (((I ⊕ Bool) ⊕ Bool) → ℕ) → ℝ) (U M : ℕ) (z : I → ℕ) :
    marginal (weightedFuture F M) U z =
      weightedFuture (marginal (fun v => F (fun t => v (swapPairs t))) U) M z := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture, OAI.ContingencyTables.IntegerWeightedTransport.swapPairs