OAI/Combinatorics/ContingencyTables/Transport/ComplementChain.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's original omission coordinates

Complementation reverses defect labels and their multipliers. We prove the actual chain energy, conditional projection, and variance identities before transferring the variance and observable inequalities back to the original factorial lift f. The final theorems assume its omission property.

  1. lemma OAI.ContingencyTables.ComplementChain.plain_complement line 22
  2. lemma OAI.ContingencyTables.ComplementChain.defect_complement line 29
  3. lemma OAI.ContingencyTables.ComplementChain.state_complement line 46
  4. lemma OAI.ContingencyTables.ComplementChain.adjacent_complement line 59
  5. def OAI.ContingencyTables.ComplementChain.complementEquiv line 91
  6. def OAI.ContingencyTables.ComplementChain.reverseMultiplier line 98
  7. lemma OAI.ContingencyTables.ComplementChain.multiplier_complement line 101
  8. lemma OAI.ContingencyTables.ComplementChain.weight_complement line 113
  9. lemma OAI.ContingencyTables.ComplementChain.chain_sum_complement line 118
  10. lemma OAI.ContingencyTables.ComplementChain.total_complement line 135
  11. lemma OAI.ContingencyTables.ComplementChain.mean_complement line 139
  12. lemma OAI.ContingencyTables.ComplementChain.variance_complement line 145
  13. lemma OAI.ContingencyTables.ComplementChain.conductance_complement line 152
  14. lemma OAI.ContingencyTables.ComplementChain.energy_complement line 158
  15. lemma OAI.ContingencyTables.ComplementChain.dirichlet_complement line 180
  16. lemma OAI.ContingencyTables.ComplementChain.plain_mass_complement line 186
  17. lemma OAI.ContingencyTables.ComplementChain.defect_mass_complement line 191
  18. lemma OAI.ContingencyTables.ComplementChain.projection_complement line 197
  19. lemma OAI.ContingencyTables.ComplementChain.slotVariance_complement line 218
  20. theorem OAI.ContingencyTables.ComplementChain.omission_twoLift_transversal_variance line 228

    Source documentation

    The actual manuscript variance theorem in original omission coordinates.

    theorem omission_twoLift_transversal_variance (gs : List (Γ × Γ)) (f g H : Set Γ → ℝ)
    (w : (Γ × Γ) → (Γ × Γ) → ℝ) (q : ℝ) (hq : 0 ≤ q)
    (hf : DegreePositive f gs.length) (hg : DegreePositive g gs.length)
    (hsigf : OmissionProperty f gs.length) (hsigg : AdditionProperty g gs.length)
    (hgs : SlotsFresh gs ∅) (hcover : pairSupport gs = Set.univ)
    (hw : ∀ p r, 0 < w p r)
    (hgood : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r →
      slotTotal gs f ∅/(4*slotDefect gs f ∅ p r) ≤ w p r)
    (hagree : ∀ S, PlainState gs S → f S = g S)
    (hcompare : ∀ S, ChainState gs S → f S ≤ q*g S) :
    slotVariance gs f H ∅ ≤ (gs.length : ℝ)*(1+8*(gs.length : ℝ)*q^2)*
      restrictedEnergy (chainEdges gs) (chainConductance gs w f) H ∅ ∅ := by
…
  21. theorem OAI.ContingencyTables.ComplementChain.omission_observable_poincare line 265

    Source documentation

    The paper's observable Poincaré theorem for the literal first factorial lift, assuming its omission property only at the actual subset degree.

    theorem omission_observable_poincare (gs : List (Γ × Γ)) (hgs : SlotsFresh gs ∅) (hne : gs ≠ [])
    (hcover : pairSupport gs = Set.univ) (w : (Γ × Γ) → (Γ × Γ) → ℝ)
    (hw : ∀ p r, 0 < w p r) (f H : Set Γ → ℝ)
    (hf : DegreePositive f gs.length) (hsig : OmissionProperty f gs.length)
    (q : ℝ) (hq : 1 ≤ q)
    (hlower : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → slotTotal gs f ∅/(4*slotDefect gs f ∅ p r) ≤ w p r)
    (hupper : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → w p r ≤ 4*slotTotal gs f ∅/slotDefect gs f ∅ p r) :
    chainVariance gs w f (observableProjection gs f H) ≤
      observableConstant gs.length q * chainDirichlet gs w f H := by
…