OAI/Analysis/DiskMaximal/SpatialLaws.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FiniteLabels.spatialRow_mixture line 58
  2. lemma OAI.FiniteLabels.spatialRow_vanish line 68
  3. abbrev OAI.ActualLabels.Label line 82
  4. instance OAI.ActualLabels.(instance at line 83) line 83
  5. instance OAI.ActualLabels.(instance at line 84) line 84
  6. lemma OAI.ActualLabels.label_unit line 86
  7. def OAI.ActualLabels.target line 88
  8. lemma OAI.ActualLabels.target_close line 90
  9. def OAI.ActualLabels.switchChance line 93
  10. lemma OAI.ActualLabels.switchChance_nonneg line 95
  11. lemma OAI.ActualLabels.switchChance_le_one line 97
  12. def OAI.ActualLabels.row line 100
  13. def OAI.ActualLabels.initial line 104
  14. lemma OAI.ActualLabels.nearby_sample_close line 108
  15. lemma OAI.ActualLabels.sampled_good line 117
  16. lemma OAI.ActualLabels.retained_good line 129
  17. lemma OAI.ActualLabels.initial_bad_zero line 142
  18. lemma OAI.ActualLabels.row_bad_zero line 151
  19. def OAI.ActualLabels.marginal line 167

    Source documentation

    The actual finite-state label marginal, with its scale-dependent spatial rows. This definition introduces no geometric or probabilistic hypothesis.

    def marginal (h : ℂ → ℂ) (r : ℕ → ℝ) : ℕ → ℂ → Law Label
  | 0,x => initial h (r 0) x
  | k+1,x => move (marginal h r k x) (row h (r (k+1)) x)

    Mentions: OAI.ActualLabels.Label, OAI.ActualLabels.initial, OAI.ActualLabels.row

  20. theorem OAI.ActualLabels.marginal_bad_zero line 171
  21. def OAI.FiniteLabels.expect line 186
  22. lemma OAI.FiniteLabels.expect_nonneg line 188
  23. lemma OAI.FiniteLabels.expect_le_one line 190
  24. lemma OAI.FiniteLabels.expect_add line 194
  25. lemma OAI.FiniteLabels.expect_sub line 197
  26. lemma OAI.FiniteLabels.expect_move line 200
  27. lemma OAI.FiniteLabels.expect_delta line 206
  28. lemma OAI.FiniteLabels.spatialRow_expect line 209
  29. lemma OAI.FiniteLabels.spatialRow_absorbing line 226

    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.FiniteLabels.expect, OAI.FiniteLabels.spatialRow

  30. def OAI.ActualLabels.badWeight line 252
  31. lemma OAI.ActualLabels.badWeight_cases line 254
  32. lemma OAI.ActualLabels.badWeight_nonneg line 256
  33. lemma OAI.ActualLabels.badWeight_le_one line 258
  34. def OAI.ActualLabels.rate line 261
  35. lemma OAI.ActualLabels.rate_nonneg line 263
  36. lemma OAI.ActualLabels.rate_le_one line 265
  37. theorem OAI.ActualLabels.row_drift line 268
  38. lemma OAI.ActualLabels.law_drift line 297
  39. def OAI.ActualLabels.switchCost line 313
  40. lemma OAI.ActualLabels.switchCost_nonneg line 317
  41. lemma OAI.ActualLabels.switchCost_le_one line 322
  42. theorem OAI.ActualLabels.switchCost_sum line 330

    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.ActualLabels.switchCost

  43. def OAI.IntrinsicMarks.activePath line 370

    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.IntrinsicMarks.Tree

  44. lemma OAI.IntrinsicMarks.activePath_valid line 377
  45. lemma OAI.IntrinsicMarks.rootEval_mono_active line 384
  46. lemma OAI.IntrinsicMarks.lateEval_mono_active line 395
  47. lemma OAI.IntrinsicMarks.particleEval_mono_active line 406
  48. def OAI.IntrinsicMarks.atPath line 412

    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.IntrinsicMarks.Tree

  49. lemma OAI.IntrinsicMarks.active_append line 418
  50. def OAI.ActualMarkTrees.lastVertex line 432
  51. def OAI.ActualMarkTrees.pathWeight line 436
  52. lemma OAI.ActualMarkTrees.pathWeight_nonneg line 440
  53. lemma OAI.ActualMarkTrees.active_length line 445
  54. lemma OAI.ActualMarkTrees.active_ne_zero line 455
  55. lemma OAI.ActualMarkTrees.atPath_tree line 467
  56. lemma OAI.ActualMarkTrees.active_hat_support line 480
  57. lemma OAI.ActualMarkTrees.lastVertex_append line 496
  58. theorem OAI.ActualMarkTrees.active_prefix_locality line 504

    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.ActualMarkTrees.tree, OAI.ActualMarkTrees.lastVertex

  59. def OAI.IntrinsicMarks.reset line 520
  60. def OAI.IntrinsicMarks.anchor line 522
  61. def OAI.IntrinsicMarks.rootAnchor line 527
  62. lemma OAI.IntrinsicMarks.anchor_zero line 530
  63. lemma OAI.IntrinsicMarks.anchor_step line 545
  64. lemma OAI.IntrinsicMarks.rootMark_cons line 567
  65. lemma OAI.IntrinsicMarks.rootAnchor_step line 571
  66. lemma OAI.IntrinsicMarks.markIndicator_cases line 581
  67. lemma OAI.IntrinsicMarks.rootMarkIndicator_cases line 590
  68. lemma OAI.IntrinsicMarks.direction_smul_pos line 598
  69. lemma OAI.IntrinsicMarks.pathCharge_sum line 608
  70. theorem OAI.ActualMarkTrees.direction_at_prefix line 629
  71. def OAI.ActualMarkTrees.pathEnergy line 649
  72. def OAI.ActualMarkTrees.pathSwitches line 652
  73. lemma OAI.ActualMarkTrees.mark_nonneg line 656
  74. theorem OAI.ActualMarkTrees.path_switch_bound line 664

    Source documentation

    The switch bound on every genuinely occupied path, using its complete intrinsic history, even before the particle's birth.

    theorem path_switch_bound {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
    (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
    (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (k : ℕ) (q : Grid N)
    {p : List (Grid N)} (hp : activePath (tree (fun q => vectorMass h r q) k 1 q) p)
    {b : ℕ} (hb : b ≤ p.length) {x : ℂ} (hx : hat r (lastVertex q p) x ≠ 0) :
    pathSwitches h r k x p b ≤ 2+
      2*pathCharge (rootMarkIndicator (1:ℂ) (1/800) (tree (fun q => vectorMass h r q) k 1 q)) p b+
      2000000*pathCharge (pathEnergy h r k q) p b := by
…

    Mentions: OAI.ActualMarkTrees.tree, OAI.ActualMarkTrees.lastVertex, OAI.ActualMarkTrees.pathSwitches, OAI.ActualMarkTrees.pathEnergy