OAI/Analysis/SignedDisk/FiniteLabels2.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedDisk.FiniteLabels.expect line 34
  2. lemma OAI.SignedDisk.FiniteLabels.expect_nonneg line 36
  3. lemma OAI.SignedDisk.FiniteLabels.expect_le_one line 38
  4. lemma OAI.SignedDisk.FiniteLabels.expect_add line 42
  5. lemma OAI.SignedDisk.FiniteLabels.expect_sub line 45
  6. lemma OAI.SignedDisk.FiniteLabels.expect_move line 48
  7. lemma OAI.SignedDisk.FiniteLabels.expect_delta line 54
  8. lemma OAI.SignedDisk.FiniteLabels.spatialRow_expect line 57
  9. lemma OAI.SignedDisk.FiniteLabels.spatialRow_absorbing line 74

    Source documentation

    An absorbing finite set gives exact drift equal to the off-diagonal switch rate. Conditions concern only tents that actually meet the point.

    lemma spatialRow_absorbing (old : ι) (target : ℤ × ℤ → ι) (p : ℤ × ℤ → ℝ)
    (hp0 : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1) (r : ℝ) (x : ℂ)
    (b : ι → ℝ) (hb : b old = 0 ∨ b old = 1)
    (ht : ∀ z, hat r z x ≠ 0 → b (target z) = 0)
    (hz : b old = 0 → ∀ z, hat r z x ≠ 0 → p z = 0) :
    expect (spatialRow old target p hp0 hp1 r x) b+interpolate r p x = b old := by
…

    Mentions: OAI.SignedDisk.FiniteLabels.expect, OAI.SignedDisk.FiniteLabels.spatialRow

  10. def OAI.SignedDisk.ActualLabels.badWeight line 100
  11. lemma OAI.SignedDisk.ActualLabels.badWeight_cases line 102
  12. lemma OAI.SignedDisk.ActualLabels.badWeight_nonneg line 104
  13. lemma OAI.SignedDisk.ActualLabels.badWeight_le_one line 106
  14. def OAI.SignedDisk.ActualLabels.rate line 109
  15. lemma OAI.SignedDisk.ActualLabels.rate_nonneg line 111
  16. lemma OAI.SignedDisk.ActualLabels.rate_le_one line 113
  17. theorem OAI.SignedDisk.ActualLabels.row_drift line 116
  18. lemma OAI.SignedDisk.ActualLabels.law_drift line 145
  19. def OAI.SignedDisk.ActualLabels.switchCost line 158
  20. lemma OAI.SignedDisk.ActualLabels.switchCost_nonneg line 162
  21. lemma OAI.SignedDisk.ActualLabels.switchCost_le_one line 167
  22. theorem OAI.SignedDisk.ActualLabels.switchCost_sum line 175

    Source documentation

    A telescoping estimate between arbitrary birth and death times. These are geometric low-energy assumptions on a path, not a switch-budget premise.

    theorem switchCost_sum (h : ℂ → ℂ) (r : ℕ → ℝ) (q : ℕ → ℤ × ℤ) (x : ℂ)
    (anchor : ℕ → ℂ) (exceptional : ℕ → Bool) {b m : ℕ} (hbm : b ≤ m)
    (hr : ∀ k ∈ Finset.Ico b m, 0 < r (k+1))
    (hx : ∀ k ∈ Finset.Ico b m, boxNorm (x-point (r (k+1)) (q (k+1))) ≤ 50*r (k+1))
    (hE : ∀ k ∈ Finset.Ico b m, exceptional (k+1) = false →
      energy h (r (k+1)) (q (k+1)) ≤ (1/1000:ℝ)^2)
    (ha : ∀ k ∈ Finset.Ico b m, exceptional (k+1) = false →
      anchor (k+1) = anchor k ∧ ‖theta h (r (k+1)) (q (k+1))-anchor k‖ ≤ 1/800) :
    (∑ k ∈ Finset.Ico b m, switchCost h r x (k+1)) ≤
      1+2*∑ k ∈ Finset.Ico b m, if exceptional (k+1) then (1:ℝ) else 0 := by
…

    Mentions: OAI.SignedDisk.ActualLabels.switchCost

  23. def OAI.SignedDisk.IntrinsicMarks.activePath line 215

    Source documentation

    Only paths ending in a nonzero terminal vector can carry particles.

    def activePath : Tree ι E → List ι → Prop
  | .leaf v, [] => v ≠ 0
  | .leaf _, _::_ => False
  | .branch _, [] => False
  | .branch t, i::p => activePath (t i) p

omit [Fintype ι] in

    Mentions: OAI.SignedDisk.IntrinsicMarks.Tree

  24. lemma OAI.SignedDisk.IntrinsicMarks.activePath_valid line 222
  25. lemma OAI.SignedDisk.IntrinsicMarks.rootEval_mono_active line 229
  26. lemma OAI.SignedDisk.IntrinsicMarks.lateEval_mono_active line 240
  27. lemma OAI.SignedDisk.IntrinsicMarks.particleEval_mono_active line 251
  28. def OAI.SignedDisk.IntrinsicMarks.atPath line 257

    Source documentation

    The subtree at a prefix (values beyond terminal nodes are immaterial).

    def atPath : Tree ι E → List ι → Tree ι E
  | t, [] => t
  | .leaf v, _::_ => .leaf v
  | .branch t, i::p => atPath (t i) p

omit [Fintype ι] in

    Mentions: OAI.SignedDisk.IntrinsicMarks.Tree

  29. lemma OAI.SignedDisk.IntrinsicMarks.active_append line 263
  30. def OAI.SignedDisk.ActualMarkTrees.lastVertex line 277
  31. def OAI.SignedDisk.ActualMarkTrees.pathWeight line 281
  32. lemma OAI.SignedDisk.ActualMarkTrees.pathWeight_nonneg line 285
  33. lemma OAI.SignedDisk.ActualMarkTrees.active_length line 290
  34. lemma OAI.SignedDisk.ActualMarkTrees.active_ne_zero line 300
  35. lemma OAI.SignedDisk.ActualMarkTrees.atPath_tree line 312
  36. lemma OAI.SignedDisk.ActualMarkTrees.active_hat_support line 325
  37. lemma OAI.SignedDisk.ActualMarkTrees.lastVertex_append line 341
  38. theorem OAI.SignedDisk.ActualMarkTrees.active_prefix_locality line 349

    Source documentation

    Actual spatial locality, at every prefix of every positive-mass particle path, for every terminal position in the genuine finest hat support.

    theorem active_prefix_locality {N : ℕ} (v : Grid N → ℂ) {r : ℝ} (hr : 0 < r)
    {k : ℕ} {b : ℝ} {q : Grid N} {p s : List (Grid N)}
    (h : activePath (tree v k b q) (p++s)) {x : ℂ}
    (hx : hat r (lastVertex q (p++s)) x ≠ 0) :
    boxNorm (x-point (scale r (k-p.length)) (lastVertex q p)) < scale r (k-p.length) := by
…

    Mentions: OAI.SignedDisk.ActualMarkTrees.tree, OAI.SignedDisk.ActualMarkTrees.lastVertex

  39. def OAI.SignedDisk.IntrinsicMarks.reset line 365
  40. def OAI.SignedDisk.IntrinsicMarks.anchor line 367
  41. def OAI.SignedDisk.IntrinsicMarks.rootAnchor line 372
  42. lemma OAI.SignedDisk.IntrinsicMarks.anchor_zero line 375
  43. lemma OAI.SignedDisk.IntrinsicMarks.anchor_step line 390
  44. lemma OAI.SignedDisk.IntrinsicMarks.rootMark_cons line 412
  45. lemma OAI.SignedDisk.IntrinsicMarks.rootAnchor_step line 416
  46. lemma OAI.SignedDisk.IntrinsicMarks.markIndicator_cases line 426
  47. lemma OAI.SignedDisk.IntrinsicMarks.rootMarkIndicator_cases line 435
  48. lemma OAI.SignedDisk.IntrinsicMarks.direction_smul_pos line 443
  49. lemma OAI.SignedDisk.IntrinsicMarks.pathCharge_sum line 453