OAI/Probability/InvariantIsing/Fields/FieldFiniteDomain.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.measurable_fieldFunction line 13
2. lemma OAI.InvariantIsing.fieldFunction_le_last line 16
3. lemma OAI.InvariantIsing.integrable_fieldFunction line 32
4. lemma OAI.InvariantIsing.integrable_path_mul_field line 39
5. lemma OAI.InvariantIsing.integral_fieldFunction line 48
6. lemma OAI.InvariantIsing.sum_finite_height_difference line 54

   Source documentation

   Summation by parts for the finite height increments.

   lemma sum_finite_height_difference (n : ℕ) (H F : ℕ → ℝ) :
       (∑ i : Fin (n + 1), (H i - if i.val = 0 then 0 else H (i.val - 1)) * F i) =
         H n * F n + ∑ i : Fin n, H i * (F i - F (i.val + 1)) := by
   …

7. lemma OAI.InvariantIsing.fieldIncrement_eq_heightSequence line 67
8. def OAI.InvariantIsing.fieldCutSequence line 77

   Source documentation

   A clamped extension used only to express finite summation by parts.

   def fieldCutSequence (h : FieldStep) (i : ℕ) : ℝ :=
   …

   Mentions: OAI.InvariantIsing.FieldStep

9. lemma OAI.InvariantIsing.fieldCutSequence_eq line 80
10. lemma OAI.InvariantIsing.fieldIncrement_weighted_sum line 84
11. lemma OAI.InvariantIsing.integral_fieldFunction_eq_increment_sum line 105
12. lemma OAI.InvariantIsing.fieldIncrement_sum line 129
13. lemma OAI.InvariantIsing.fieldPairing_le_const_integral line 134
14. lemma OAI.InvariantIsing.field_majorant_coefficient_le_one line 143
15. lemma OAI.InvariantIsing.fieldValue_add_pairing_le line 153

    Source documentation

    The exact entropy cap needed for finite-step trial paths below one.

    lemma fieldValue_add_pairing_le (p : OverlapPath) {d : ℝ} (hd : 0 < d) (hd1 : d ≤ 1)
        (hp : ∀ᵐ s ∂pathMeasure, p s ≤ 1 - d) (h : FieldStep) :
        fieldValue h 0 + fieldPairing p h / 2 ≤ (d⁻¹ - 1) * Real.log 2 := by
    …

    Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue, OAI.InvariantIsing.fieldPairing

16. lemma OAI.InvariantIsing.entropyFunctional_le_of_bounded line 189
17. lemma OAI.InvariantIsing.entropyFunctional_ne_top_of_bounded line 196
18. lemma OAI.InvariantIsing.entropyFunctional_mono line 201