OAI/Computability/UniqueGames/Reduction/WeightedSource.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource line 20
2. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.denominator line 32
3. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.denominator_positive line 34
4. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.den_dvd_denominator line 37
5. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.numerator line 41
6. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.numerator_cast line 44
7. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.weight_eq_ratio line 61

   Source documentation

   Exact rational-to-integer conversion, not an approximation.

   theorem weight_eq_ratio (i : Fin S.occurrences) :
       S.weight i = (S.numerator i : ℚ) / S.denominator := by
   …

8. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.numerators line 67
9. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.length_numerators line 69
10. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.sum_numerators line 72
11. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.equationAt line 78
12. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.equationAt_fin line 81
13. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundedEquations line 84
14. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundedEquations_length line 87
15. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundedEquations_nonempty line 91
16. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundedEquations_origin line 99

    Source documentation

    Rounding copies complete equation records without altering any of their slots.

    theorem roundedEquations_origin (D : Nat) (e : Eqn) (he : e ∈ S.roundedEquations D) :
        ∃ i : Fin S.occurrences, e = S.equation i := by
    …

17. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.weightedValue line 108
18. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundedValue line 111
19. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.selectedSum_ofFn line 116
20. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.selectedMass_cast line 129
21. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundedValue_bounds line 139
22. def OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundingDenominator line 181

    Source documentation

    ceil(4m/γ) computed from the exact numerator and denominator of γ.

    def roundingDenominator (γ : ℚ) : Nat :=
    …

23. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundingDenominator_positive line 184
24. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundingDenominator_budget line 189
25. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundingDenominator_size line 210
26. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.completeness_transport line 214
27. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.soundness_transport line 221
28. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.RationalSource.roundedEquations_for_nonempty line 229
29. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.e3lin_completeness line 239
30. theorem OAI.UniqueGamesTheorem.Reduction.WeightedSource.e3lin_soundness line 255