OAI/Probability/InvariantIsing/Fields/FieldRefineCut.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Splitting one interval of a finite field without changing its height.

  1. lemma OAI.InvariantIsing.field_ofFn_insertNth line 15
  2. def OAI.InvariantIsing.fieldSplitHeight line 33

    Source documentation

    Duplicate the old height on both sides of the new cut.

    def fieldSplitHeight (h : FieldStep) (i : Fin (h.depth + 1))
    (j : Fin (h.depth + 2)) : ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  3. lemma OAI.InvariantIsing.fieldSplitHeight_nonneg line 38
  4. lemma OAI.InvariantIsing.fieldSplitHeight_monotone line 43
  5. def OAI.InvariantIsing.fieldInsertCut line 50

    Source documentation

    Inserting a cut strictly inside one existing cell keeps the field path unchanged.

    def fieldInsertCut (h : FieldStep) (i : Fin (h.depth + 1)) (c : ℝ)
    (hc₀ : h.cut i.castSucc < c) (hc₁ : c < h.cut i.succ) : FieldStep where
…

    Mentions: OAI.InvariantIsing.FieldStep

  6. lemma OAI.InvariantIsing.fieldInsertCut_depth line 68
  7. lemma OAI.InvariantIsing.fieldInsertCut_last_height line 72
  8. lemma OAI.InvariantIsing.fieldInsertCut_cut_below line 81
  9. lemma OAI.InvariantIsing.fieldInsertCut_cut_at line 91
  10. lemma OAI.InvariantIsing.fieldInsertCut_cut_above line 97
  11. lemma OAI.InvariantIsing.fieldInsertCut_height_below line 106
  12. lemma OAI.InvariantIsing.fieldInsertCut_height_above line 112