WordWeightBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.LowerParameters.sum_actual_weight_le_exp_of_parameters line 14

Source documentation

The actual rounded parameters discharge every numerical and run-product premise of the corrected word sum. Only the chosen schedule remains an input.

theorem sum_actual_weight_le_exp_of_parameters {n : ℕ} (hn : 16 ≤ n + 1)
    (edges : Finset (Fin (n + 1) × Fin (n + 1)))
    (V S : Finset (Fin (n + 1))) (R : Fin (n + 1) → Fin (n + 1) → Prop)
    (hS : S ⊆ V) (hV : ∀ i ∈ V, ∀ j, R i j → j ∉ V)
    (hR : ∀ e ∈ edges, R e.1 e.2 ∧ R e.2 e.1)
    (hdegree : ∀ i ∈ S, SwitchRestoration.endpointDegree edges i = 2)
    (hswitch : ∀ w, SwitchRestoration.switchCount edges w = (WordSwitches.switches w).card)
    (hend : (V \ S).card ≤ 1)
    (hcard : 2 * (V.card : ℝ) ≤ ((n + 1 : ℕ) : ℝ))
    (hdiscrepancy : ∀ l : List (Fin (n + 1)), l <:+: List.ofFn id →
      (l.countP (fun i => decide (i ∈ V)) : ℝ) -
        rho (n + 1) * l.countP (fun i => !decide (i ∈ V)) ≤ 1 + rho (n + 1)) :
…

Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.WordSwitches.switches, OAI.Problem335.LowerParameters.rho