EqualityReindex.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Equality factors under the actual physical coordinate bijection

A bijection of coordinates preserves the line totals and unary products. Consequently the balanced marginal signature applies to the literal physical factor family after all cell-index bookkeeping has been proved.

lemma OAI.ContingencyTables.EqualityReindex.lineTotal_reindex line 21
lemma OAI.ContingencyTables.EqualityReindex.productWeight_reindex line 27
lemma OAI.ContingencyTables.EqualityReindex.exactWeight_reindex line 37

theorem OAI.ContingencyTables.EqualityReindex.physical_marginal_removal line 50

Source documentation

The application needs precisely the raw removal signature of the actual physical factor marginal, rather than a hypothesis asserting it.

theorem physical_marginal_removal (Ms : List ℕ) (m : S → ℕ) (R : ℕ)
    (e : Coordinates S Ms ≃ D) (line : D → G) (root : G → Bool)
    (rate offset slope : G → ℝ) (urate ell uslope cap : D → ℝ)
    (hwidth : ∀ M ∈ Ms, 2≤M) (hrate : ∀ g, 0≤rate g) (hu : ∀ d, 0≤urate d) :
    RemovalSlice (eliminate Ms (fun z =>
      exactWeight line root rate offset slope urate ell uslope cap (z ∘ e.symm))) m R := by
…

theorem OAI.ContingencyTables.EqualityReindex.physical_marginal_reflected line 67

Source documentation

Global physical reflection also preserves the proved marginal signature, and all balanced pairs are reflected along with small views.

theorem physical_marginal_reflected (Ms : List ℕ) (m : S → ℕ) (R : ℕ)
    (e : Coordinates S Ms ≃ D) (line : D → G) (root : G → Bool)
    (rate offset slope : G → ℝ) (urate ell uslope cap : D → ℝ)
    (hwidth : ∀ M ∈ Ms, 2≤M) (hrate : ∀ g, 0≤rate g) (hu : ∀ d, 0≤urate d) :
    RemovalSlice (fun z => eliminate Ms (fun q =>
      exactWeight line root rate offset slope urate ell uslope cap (q ∘ e.symm))
      (IntegerReflection.reflect m z)) m R := by
…

Mentions: OAI.ContingencyTables.IntegerReflection.reflect