OAI/Algebra/DepthFive/PathIsolatedWeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.PathIsolatedWeight.adjacent line 12

   Source documentation

   Adjacent positions of the path, in either orientation.

   def adjacent {n : ℕ} (i j : Fin (n + 1)) : Prop :=
   …

2. def OAI.Problem335.PathIsolatedWeight.interior line 16

   Source documentation

   Interior selected positions are exactly those eligible for the two-switch flip.

   def interior {n : ℕ} (V : Finset (Fin (n + 1))) : Finset (Fin (n + 1)) :=
   …

3. theorem OAI.Problem335.PathIsolatedWeight.interior_subset line 19
4. theorem OAI.Problem335.PathIsolatedWeight.pathEdges_adjacent line 22
5. theorem OAI.Problem335.PathIsolatedWeight.independent_of_no_adjacent line 30
6. theorem OAI.Problem335.PathIsolatedWeight.endpointDegree_interior line 44
7. theorem OAI.Problem335.PathIsolatedWeight.exceptional_subset_first line 50
8. theorem OAI.Problem335.PathIsolatedWeight.exceptional_card_le_one line 65
9. theorem OAI.Problem335.PathIsolatedWeight.switchCount_eq_wordSwitches line 69
10. theorem OAI.Problem335.PathIsolatedWeight.sum_weight_le_uniform line 76

    Source documentation

    Correction removal for the concrete path: all graph hypotheses are discharged.

    theorem sum_weight_le_uniform {n : ℕ} (V : Finset (Fin (n + 1)))
        (hV : ∀ i : Fin n, ¬ (i.castSucc ∈ V ∧ i.succ ∈ V))
        (hlast : Fin.last n ∉ V)
        {A B x : ℝ} (hA : 1 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x) (hx1 : x ≤ 1) :
        (∑ w : Fin (n + 1) → Bool,
          IsolatedWeight.weight (SwitchRestoration.pathEdges n) V adjacent A B x w) ≤
          (1 + 2 * x ^ 2) ^ V.card * (1 + A) * (1 + A * x) ^ V.card *
            ∑ w : Fin (n + 1) → Bool,
              IsolatedWeight.baseWeight (SwitchRestoration.pathEdges n) V A B x w := by
    …

    Mentions: OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.SwitchRestoration.pathEdges, OAI.Problem335.PathIsolatedWeight.adjacent, OAI.Problem335.IsolatedWeight.baseWeight