OAI/Probability/InvariantIsing/Fields/FieldHeightChart.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Coordinate charts for the exact finite field functional. The charts use its original Gaussian increments and change a single covariance height.

  1. def OAI.InvariantIsing.fieldAllIncrements line 15
  2. lemma OAI.InvariantIsing.fieldAllIncrements_length line 19
  3. lemma OAI.InvariantIsing.fieldAllIncrements_value line 22
  4. lemma OAI.InvariantIsing.fieldAllIncrements_strict line 30
  5. lemma OAI.InvariantIsing.list_split_two line 37
  6. def OAI.InvariantIsing.fieldInteriorChart line 46

    Source documentation

    This changes the height at an interior cell, keeping the final height and every other increment fixed.

    def fieldInteriorChart (h : FieldStep) (i : Fin h.depth) (t z : ℝ) : ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  7. lemma OAI.InvariantIsing.interior_list_zero line 54
  8. lemma OAI.InvariantIsing.fieldInteriorChart_zero line 83
  9. def OAI.InvariantIsing.fieldFinalChart line 91

    Source documentation

    The analogous final-height chart changes the last increment and the normalizing diagonal covariance together.

    def fieldFinalChart (h : FieldStep) (t z : ℝ) : ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  10. lemma OAI.InvariantIsing.fieldAllIncrements_root line 98
  11. lemma OAI.InvariantIsing.fieldAllSquares_magnetization line 109
  12. lemma OAI.InvariantIsing.terminal_list_zero line 128
  13. lemma OAI.InvariantIsing.fieldFinalChart_zero line 149
  14. lemma OAI.InvariantIsing.hasDerivAt_fieldInteriorChart line 155
  15. lemma OAI.InvariantIsing.hasDerivAt_fieldInteriorChart_magnetization line 185

    Source documentation

    The exact interior coordinate gradient in fld:gradient, expressed with the already constructed physical magnetization-overlap levels.

    lemma hasDerivAt_fieldInteriorChart_magnetization (h : FieldStep) (i : Fin h.depth)
    (hstrict : ∀ j, 0 < (fieldIncrement h j).2) :
    HasDerivAt (fun t => fieldInteriorChart h i t 0)
      (-(h.cut i.castSucc.succ - h.cut i.castSucc.castSucc) / 2 *
        fieldMagnetizationLevel h i.castSucc) 0 := by
…

    Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldIncrement, OAI.InvariantIsing.fieldInteriorChart, OAI.InvariantIsing.fieldMagnetizationLevel

  16. lemma OAI.InvariantIsing.hasDerivAt_fieldFinalChart line 199