OAI/Computability/MaxCut/Machines/AlphabetBudget.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Conversion of the actual selected-label information bound into the alphabet budget, followed by finite averaging over unused coordinates.

  1. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLabels_card line 20
  2. theorem OAI.MaxCutGames.Foundations.Repetition.unusedCoordinates_card line 25
  3. theorem OAI.MaxCutGames.Foundations.Repetition.unusedCoordinates_card_real line 30
  4. theorem OAI.MaxCutGames.Foundations.Repetition.log_le_logTwo line 35
  5. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLabels_log_le line 44
  6. theorem OAI.MaxCutGames.Foundations.Repetition.selectedInformationRadius_le line 59

    Source documentation

    The actual selected-label radius is bounded by the base-two alphabet budget. The unused-coordinate factor is a real subtraction, as in the scalar recurrence.

    theorem selectedInformationRadius_le [Nonempty A₁] [Nonempty A₂]
    (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (ell : ℝ)
    (hell : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell) :
    selectedInformationRadius G strategy selected ≤
      Real.sqrt (((n : ℝ) - selected.card) *
        ((selected.card : ℝ) * ell + logTwo (1 / G.selectedSuccess strategy selected))) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.logTwo, OAI.MaxCutGames.Foundations.Repetition.selectedInformationRadius

  7. theorem OAI.MaxCutGames.Foundations.Repetition.sqrt_budget_factor line 78
  8. theorem OAI.MaxCutGames.Foundations.Repetition.exists_coordinate_le_information_budget line 88

    Source documentation

    An actual finite average over all unused coordinates yields the numerical bound needed by the selected-success recurrence. No sign condition on the individual errors is required.

    theorem exists_coordinate_le_information_budget [Nonempty A₁] [Nonempty A₂]
    (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (ell : ℝ)
    (hell : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell)
    (hselected : selected.card < n)
    (error : {i : Fin n // i ∉ selected} → ℝ)
    (hsum : (∑ j, error j) ≤ 15 * selectedInformationRadius G strategy selected) :
    ∃ j : {i : Fin n // i ∉ selected}, error j ≤ 15 * Real.sqrt
      (((selected.card : ℝ) * ell + logTwo (1 / G.selectedSuccess strategy selected)) /
        ((n : ℝ) - selected.card)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.logTwo, OAI.MaxCutGames.Foundations.Repetition.selectedInformationRadius