OAI/Computability/MaxCut/Arithmetic/GridWeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OptimalMaxCut.LongCode.Law.gridWeight line 17

   Source documentation

   Downward rounding is performed BEFORE aggregation. Thus every output mass has the same polynomially sized integer denominator; no product of all input vertex degrees has to be represented as a unary integer.

   noncomputable def gridWeight (P : ℕ) (a : ℚ) : ℚ := (⌊(P : ℚ) * a⌋₊ : ℚ) / P

2. theorem OAI.OptimalMaxCut.LongCode.Law.gridWeight_nonneg line 19
3. theorem OAI.OptimalMaxCut.LongCode.Law.gridWeight_le line 22
4. theorem OAI.OptimalMaxCut.LongCode.Law.gridWeight_error line 28
5. def OAI.OptimalMaxCut.LongCode.Law.grid line 37
6. theorem OAI.OptimalMaxCut.LongCode.Law.grid_average line 50
7. theorem OAI.OptimalMaxCut.LongCode.Law.grid_average_bounds line 55
8. def OAI.OptimalMaxCut.LongCode.roundedWeights line 79

   Source documentation

   Lost mass becomes a loop, which is deleted by exactly the original aggregation. It is never renormalized into non-loop edges.

   noncomputable def roundedWeights {I : Type} [Fintype I] {N : ℕ}
       (p : Law I) (endpoints : I → Fin N × Fin N) (v0 : Fin N)
       (P : ℕ) (hP : 0 < P) : Fin N → Fin N → ℚ :=
   …

   Mentions: OAI.OptimalMaxCut.LongCode.Law

9. theorem OAI.OptimalMaxCut.LongCode.roundedWeights_cut_error line 86
10. theorem OAI.OptimalMaxCut.LongCode.roundedWeights_max_error line 100