OAI/Combinatorics/ContingencyTables/Counting/CompanionAnnealing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Adjacent actual companion weights and ideal multipliers

The parameter step is 1/(H/A). Its factor-two bounds are proved from the literal forest penalty bound, then passed to the actual labelled weights and their exact transversal/defect totals.

  1. def OAI.ContingencyTables.CompanionAnnealing.scale line 22
  2. lemma OAI.ContingencyTables.CompanionAnnealing.scale_positive line 24
  3. lemma OAI.ContingencyTables.CompanionAnnealing.source_parameter line 33

    Source documentation

    The source's j*A/H parameter is exactly j/(H/A), for its literal integer H=10*A*d²*(W+1). The arbitrary positive penalty coefficient therefore cancels from every adjacent-phase estimate below.

    lemma source_parameter (A : Instance I J) (coefficient j : ℕ) (hc : 0< coefficient) :
    (j:ℝ)*(coefficient:ℝ)/((10*coefficient*A.d^2*(A.W+1):ℕ):ℝ)=
      (j:ℝ)/scale A := by
…

    Mentions: OAI.ContingencyTables.CompanionAnnealing.scale

  4. def OAI.ContingencyTables.CompanionAnnealing.weight line 45
  5. theorem OAI.ContingencyTables.CompanionAnnealing.count_adjacent line 48
  6. theorem OAI.ContingencyTables.CompanionAnnealing.weight_positive line 85
  7. theorem OAI.ContingencyTables.CompanionAnnealing.weight_adjacent line 90
  8. theorem OAI.ContingencyTables.CompanionAnnealing.total_adjacent line 106
  9. theorem OAI.ContingencyTables.CompanionAnnealing.ideal_adjacent line 115