OAI/Algebra/DepthFive/IsolatedWeight.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.IsolatedWeight.falseNeighbors line 14

   Source documentation

   Internal neighboring positions of the same normal (false) type.

   def falseNeighbors (R : ι → ι → Prop) (w : ι → Bool) (i : ι) : Finset ι := by
   …

2. def OAI.Problem335.IsolatedWeight.correction line 19

   Source documentation

   The coincidence correction factors at the normal V positions.

   def correction (V : Finset ι) (R : ι → ι → Prop) (A x : ℝ)
       (w : ι → Bool) : ℝ := by
   …

3. theorem OAI.Problem335.IsolatedWeight.falseNeighbors_unset line 27

   Source documentation

   Restoring any subset of an independent V set does not change the neighbors of any V position. Endpoints are allowed in V.

   theorem falseNeighbors_unset {V T : Finset ι} {R : ι → ι → Prop}
       (hT : T ⊆ V) (hV : ∀ i ∈ V, ∀ j, R i j → j ∉ V)
       (w : ι → Bool) {i : ι} (hi : i ∈ V) :
       falseNeighbors R (IsolatedFlip.unset w T) i = falseNeighbors R w i := by
   …

   Mentions: OAI.Problem335.IsolatedWeight.falseNeighbors, OAI.Problem335.IsolatedFlip.unset

4. theorem OAI.Problem335.IsolatedWeight.falseNeighbors_eq_empty line 39
5. theorem OAI.Problem335.IsolatedWeight.falseVertices_unset line 52

   Source documentation

   The normal V positions after restoration consist of the old normal positions together with the restored subset.

   theorem falseVertices_unset {V T : Finset ι} (hT : T ⊆ V)
       (w : ι → Bool) :
       (V.filter fun i => IsolatedFlip.unset w T i = false) =
         (V.filter fun i => w i = false) ∪ T := by
   …

   Mentions: OAI.Problem335.IsolatedFlip.unset

6. theorem OAI.Problem335.IsolatedWeight.falseVertices_disjoint line 63
7. theorem OAI.Problem335.IsolatedWeight.correction_unset line 75

   Source documentation

   The exact local correction-product factor in the isolated-position flip. Every restored position has no normal neighbors, and hence contributes 1+A.

   theorem correction_unset {V T : Finset ι} {R : ι → ι → Prop}
       (hT : T ⊆ V) (hV : ∀ i ∈ V, ∀ j, R i j → j ∉ V)
       (w : ι → Bool) (hw : ∀ i ∈ T, w i = true)
       (hnear : ∀ i ∈ T, ∀ j, R i j → w j = true) (A x : ℝ) :
       correction V R A x (IsolatedFlip.unset w T) =
         correction V R A x w * (1 + A) ^ T.card := by
   …

   Mentions: OAI.Problem335.IsolatedWeight.correction, OAI.Problem335.IsolatedFlip.unset

8. theorem OAI.Problem335.IsolatedWeight.complement_trueVertices_unset line 98

   Source documentation

   True positions in the complementary variable group are unchanged.

   theorem complement_trueVertices_unset {V T : Finset ι} (hT : T ⊆ V)
       (w : ι → Bool) :
       ((Finset.univ \ V).filter fun i => IsolatedFlip.unset w T i = true) =
         ((Finset.univ \ V).filter fun i => w i = true) := by
   …

   Mentions: OAI.Problem335.IsolatedFlip.unset

9. def OAI.Problem335.IsolatedWeight.weight line 111

   Source documentation

   The actual weighted word summand, with A = alpha⁻¹, B = beta, and x = n⁻¹. The relation records internal adjacency.

   def weight (edges : Finset (ι × ι)) (V : Finset ι) (R : ι → ι → Prop)
       (A B x : ℝ) (w : ι → Bool) : ℝ := by
   …

10. theorem OAI.Problem335.IsolatedWeight.weight_unset line 122

    Source documentation

    Exact isolated-flip weight identity given the switch-count increment. The switch increment is supplied by switchCount_restore_eq_add_twice_card. No bound or positivity is needed except nonvanishing of the D-layer weight.

    theorem weight_unset {edges : Finset (ι × ι)} {V T : Finset ι}
        {R : ι → ι → Prop} (hT : T ⊆ V)
        (hV : ∀ i ∈ V, ∀ j, R i j → j ∉ V)
        (w : ι → Bool) (hw : ∀ i ∈ T, w i = true)
        (hnear : ∀ i ∈ T, ∀ j, R i j → w j = true)
        (hswitch : SwitchRestoration.switchCount edges (IsolatedFlip.unset w T) =
          SwitchRestoration.switchCount edges w + 2 * T.card)
        {A : ℝ} (hA : A ≠ 0) (B x : ℝ) :
        weight edges V R A B x (IsolatedFlip.unset w T) =
          weight edges V R A B x w * (x ^ 2 * (1 + A) / A) ^ T.card := by
    …

    Mentions: OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.IsolatedFlip.unset, OAI.Problem335.IsolatedWeight.weight

11. theorem OAI.Problem335.IsolatedWeight.weight_flip line 144

    Source documentation

    The isolated-flip identity for the actual word weight. Only interior positions (of edge degree two) may flip, while V may also contain endpoints.

    theorem weight_flip {edges : Finset (ι × ι)} {V S : Finset ι}
        {R : ι → ι → 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)
        {A : ℝ} (hA : A ≠ 0) (B x : ℝ) (w : ι → Bool) :
        weight edges V R A B x w =
          weight edges V R A B x (IsolatedFlip.flip S R w) *
            (x ^ 2 * (1 + A) / A) ^ (IsolatedFlip.removed S R w).card := by
    …

    Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.IsolatedFlip.flip, OAI.Problem335.IsolatedFlip.removed

12. theorem OAI.Problem335.IsolatedWeight.weight_nonneg line 181

    Source documentation

    Nonnegative parameters give a nonnegative word weight.

    theorem weight_nonneg (edges : Finset (ι × ι)) (V : Finset ι)
        (R : ι → ι → Prop) {A B x : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x)
        (w : ι → Bool) : 0 ≤ weight edges V R A B x w := by
    …

    Mentions: OAI.Problem335.IsolatedWeight.weight

13. theorem OAI.Problem335.IsolatedWeight.sum_weight_le_fixed line 190

    Source documentation

    Summing the exact word-weight identity over the fibers removes all isolated positions at a multiplicative cost (1+x²(1+A)/A)^|S|.

    theorem sum_weight_le_fixed {edges : Finset (ι × ι)} {V S : Finset ι}
        {R : ι → ι → 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)
        {A B x : ℝ} (hA : 0 < A) (hB : 0 ≤ B) (hx : 0 ≤ x) :
        (∑ w : ι → Bool, weight edges V R A B x w) ≤
          (1 + x ^ 2 * (1 + A) / A) ^ S.card *
            ∑ w ∈ Finset.univ.filter (fun w => IsolatedFlip.flip S R w = w),
              weight edges V R A B x w := by
    …

    Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.IsolatedFlip.flip

14. theorem OAI.Problem335.IsolatedWeight.falseNeighbors_card_pos_of_fixed line 210

    Source documentation

    A normal position in the flip set of a fixed word has at least one normal neighbor: otherwise the canonical flip would change it.

    theorem falseNeighbors_card_pos_of_fixed {S : Finset ι} {R : ι → ι → Prop}
        {w : ι → Bool} (hw : IsolatedFlip.flip S R w = w)
        {i : ι} (hi : i ∈ S) (hwi : w i = false) :
        0 < (falseNeighbors R w i).card := by
    …

    Mentions: OAI.Problem335.IsolatedFlip.flip, OAI.Problem335.IsolatedWeight.falseNeighbors

15. theorem OAI.Problem335.IsolatedWeight.correction_le_of_fixed line 227

    Source documentation

    The coincidence correction of a word with no isolated eligible position. The exceptional positions V \ S include the external endpoint.

    theorem correction_le_of_fixed {V S : Finset ι} {R : ι → ι → Prop}
        (hS : S ⊆ V) {w : ι → Bool} (hw : IsolatedFlip.flip S R w = w)
        {A x : ℝ} (hA : 0 ≤ A) (hx : 0 ≤ x) (hx1 : x ≤ 1) :
        correction V R A x w ≤
          (1 + A * x) ^ S.card * (1 + A) ^ (V \ S).card := by
    …

    Mentions: OAI.Problem335.IsolatedFlip.flip, OAI.Problem335.IsolatedWeight.correction

16. theorem OAI.Problem335.IsolatedWeight.correction_le_endpoint_bound line 268

    Source documentation

    With at most one exceptional V endpoint, the fixed-word correction has the exact uniform bound used in the manuscript.

    theorem correction_le_endpoint_bound {V S : Finset ι} {R : ι → ι → Prop}
        (hS : S ⊆ V) (hend : (V \ S).card ≤ 1)
        {w : ι → Bool} (hw : IsolatedFlip.flip S R w = w)
        {A x : ℝ} (hA : 0 ≤ A) (hx : 0 ≤ x) (hx1 : x ≤ 1) :
        correction V R A x w ≤ (1 + A) * (1 + A * x) ^ V.card := by
    …

    Mentions: OAI.Problem335.IsolatedFlip.flip, OAI.Problem335.IsolatedWeight.correction

17. def OAI.Problem335.IsolatedWeight.baseWeight line 285

    Source documentation

    The word summand without coincidence corrections.

    def baseWeight (edges : Finset (ι × ι)) (V : Finset ι) (A B x : ℝ)
        (w : ι → Bool) : ℝ :=
    …

18. theorem OAI.Problem335.IsolatedWeight.weight_eq_baseWeight line 291
19. theorem OAI.Problem335.IsolatedWeight.baseWeight_nonneg line 295
20. theorem OAI.Problem335.IsolatedWeight.sum_weight_le_uncorrected line 303

    Source documentation

    Complete isolated-position correction removal, including the exceptional endpoint factor and enlargement of the fixed-word sum to all words.

    theorem sum_weight_le_uncorrected {edges : Finset (ι × ι)} {V S : Finset ι}
        {R : ι → ι → 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)
        (hend : (V \ S).card ≤ 1)
        {A B x : ℝ} (hA : 0 < A) (hB : 0 ≤ B) (hx : 0 ≤ x) (hx1 : x ≤ 1) :
        (∑ w : ι → Bool, weight edges V R A B x w) ≤
          (1 + x ^ 2 * (1 + A) / A) ^ S.card *
            (1 + A) * (1 + A * x) ^ V.card *
              ∑ w : ι → Bool, baseWeight edges V A B x w := by
    …

    Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.IsolatedWeight.baseWeight

21. theorem OAI.Problem335.IsolatedWeight.sum_weight_le_uniform_uncorrected line 345

    Source documentation

    The uniform correction-removal inequality in the form used by the word-sum estimate: A ≥ 1 bounds the flip cost by 1+2*x².

    theorem sum_weight_le_uniform_uncorrected {edges : Finset (ι × ι)} {V S : Finset ι}
        {R : ι → ι → 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)
        (hend : (V \ S).card ≤ 1)
        {A B x : ℝ} (hA : 1 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x) (hx1 : x ≤ 1) :
        (∑ w : ι → Bool, weight edges V R A B x w) ≤
          (1 + 2 * x ^ 2) ^ V.card * (1 + A) * (1 + A * x) ^ V.card *
            ∑ w : ι → Bool, baseWeight edges V A B x w := by
    …

    Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.IsolatedWeight.baseWeight