OAI/Probability/InvariantIsing/Cavity/CavityFiniteDeficit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The deficit and cumulative masses of a genuine finite overlap quantile, with atoms retained at all cell values.

  1. lemma OAI.InvariantIsing.ae_finite_overlap_cell line 16
  2. lemma OAI.InvariantIsing.finite_overlap_value_mem_unit line 27
  3. lemma OAI.InvariantIsing.finite_overlap_ae_bounds line 36
  4. lemma OAI.InvariantIsing.finite_overlap_deficit_pos line 47
  5. theorem OAI.InvariantIsing.finite_overlap_cumulative_mass line 57
  6. theorem OAI.InvariantIsing.finite_overlap_value_gap line 89
  7. theorem OAI.InvariantIsing.finite_overlap_deficit_increment line 106

    Source documentation

    The actual finite-level deficit increment, including the atoms at both neighboring overlap values.

    theorem finite_overlap_deficit_increment {n : ℕ} (p : OverlapPath)
    (cut : Fin (n + 2) → ℝ) (hcut : StrictMono cut)
    (hfirst : cut 0 = 0) (hlast : cut (Fin.last (n + 1)) = 1)
    (q : Fin (n + 1) → ℝ) (hq : StrictMono q)
    (hp : ∀ j s, s ∈ Ioo (cut j.castSucc) (cut j.succ) → p s = q j)
    (i : Fin n) {r : ℝ} (hr : r ∈ Icc (q i.castSucc) (q i.succ)) :
    deficit p r = deficit p (q i.castSucc) -
      cut i.succ.castSucc * (r - q i.castSucc) := by
…

    Mentions: OAI.InvariantIsing.OverlapPath