OAI/Analysis/SignedDisk/PhysicalCells1.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedDisk.PhysicalCells.derivative_majorant_integral line 31
  2. lemma OAI.SignedDisk.PhysicalCells.value_majorant_integral line 40
  3. lemma OAI.SignedDisk.DiskMoments.average_gradient_norm_le line 51
  4. lemma OAI.SignedDisk.DiskMoments.average_gradient_negative_le line 59
  5. lemma OAI.SignedDisk.DiskMoments.physical_gradient_norm_majorant line 70
  6. lemma OAI.SignedDisk.DiskMoments.physical_gradient_negative_majorant line 81
  7. theorem OAI.SignedDisk.CommonPrices.physical_directional_price line 98
  8. theorem OAI.SignedDisk.CommonPrices.physical_size_price line 134
  9. theorem OAI.SignedDisk.CommonPrices.physical_value_price line 170
  10. lemma OAI.SignedDisk.DiskMoments.signedAverage_abs_le line 200
  11. def OAI.SignedDisk.DiskMoments.oscillationSet line 211
  12. def OAI.SignedDisk.DiskMoments.oscillation line 213
  13. lemma OAI.SignedDisk.DiskMoments.oscillationSet_zero line 215
  14. lemma OAI.SignedDisk.DiskMoments.oscillationSet_bdd line 217
  15. lemma OAI.SignedDisk.DiskMoments.oscillation_nonneg line 226
  16. lemma OAI.SignedDisk.DiskMoments.le_oscillation line 229
  17. lemma OAI.SignedDisk.DiskMoments.oscillation_majorant line 233
  18. def OAI.SignedDisk.SignedRuns.runEnvelope line 251
  19. lemma OAI.SignedDisk.SignedRuns.radius_antitone line 254
  20. lemma OAI.SignedDisk.SignedRuns.runEnvelope_attains line 260
  21. lemma OAI.SignedDisk.SignedRuns.runEnvelope_le_next line 268
  22. lemma OAI.SignedDisk.SignedRuns.runEnvelope_extension_bound line 276
  23. lemma OAI.SignedDisk.SignedRuns.runEnvelope_new_bound line 302
  24. def OAI.SignedDisk.SignedRuns.activeStart line 313

    Source documentation

    Reversed chronological histories. The active run's start is retained when its new label agrees, and is reset to the new time at a switch.

    def activeStart : List Label → ℕ
  | [] => 0
  | [_] => 0
  | n::old::p => if n = old then activeStart (old::p) else (old::p).length
  25. lemma OAI.SignedDisk.SignedRuns.activeStart_le line 318
  26. def OAI.SignedDisk.SignedRuns.potential line 329

    Source documentation

    The exact closed-prefix vector potential, updated without ever taking the absolute size of an old large-radius envelope.

    def potential (x : ℂ) : List Label → ℂ
  | [] => 0
  | [n] => (runEnvelope g r 0 0 x-signedAverage g x (r 0)) • (n:ℂ)
  | n::old::p => potential x (old::p)+
      (if n = old then (runEnvelope g r (activeStart (old::p)) (p.length+1) x-
        runEnvelope g r (activeStart (old::p)) p.length x) • (n:ℂ)
      else (runEnvelope g r (p.length+1) (p.length+1) x-
        signedAverage g x (r (p.length+1))) • (n:ℂ))

    Mentions: OAI.SignedDisk.SignedRuns.runEnvelope, OAI.SignedDisk.SignedRuns.activeStart

  27. lemma OAI.SignedDisk.SignedRuns.potential_increment line 338
  28. theorem OAI.SignedDisk.SignedRuns.potential_continuation_bound line 355
  29. def OAI.SignedDisk.SignedRuns.jet line 383

    Source documentation

    The actual closed-prefix potentials at the leaves, with the stochastic row jet at every observation time.

    def jet : ℕ → List Label → Label → JetTree Label ℂ
  | 0,p,_ => .leaf (potential g r x p)
  | d+1,p,n => .branch (J p.length n) (potential g r x p)
      (∑ k ∈ Ico p.length (p.length+d+1), v k) (fun a => jet d (a::p) a)

    Mentions: OAI.SignedDisk.SignedRuns.potential

  30. lemma OAI.SignedDisk.SignedRuns.jet_terminalBound line 388
  31. lemma OAI.SignedDisk.SignedRuns.jet_controlled line 400
  32. def OAI.SignedDisk.SignedRuns.rewardCost line 418

    Source documentation

    Backward expected reward for an arbitrary time-dependent finite Markov law.

    def rewardCost (reward : ℕ → Label → ℝ) : ℕ → ℕ → Label → ℝ
  | _,0,_ => 0
  | k,d+1,n => reward k n+expect (J k n).law (fun a => rewardCost reward (k+1) d a)
  33. lemma OAI.SignedDisk.SignedRuns.jet_cost line 422
  34. lemma OAI.SignedDisk.SignedRuns.expect_rewardCost line 437
  35. theorem OAI.SignedDisk.SignedRuns.run_signed_flux_bound line 453

    Source documentation

    Signed finite-history flux with the actual run potential and the exact forward stochastic marginal law. No old large-radius envelope is priced.

    theorem run_signed_flux_bound (hg : ContDiff ℝ 1 g) (hr : ∀ k, 0 < r k)
    (hstep : ∀ k, 2*r (k+1) = r k)
    (hv : ∀ k t t', 0 < t → t ≤ 4*r k → 0 < t' → t' ≤ 4*r k →
      |DiskMoments.signedAverage g x t-DiskMoments.signedAverage g x t'| ≤ v k)
    (m : ℕ) (old : Label) (μ : ℕ → Law Label) (hμ0 : μ 0 = delta old)
    (hμ : ∀ k, μ (k+1) = move (μ k) (fun n => (J k n).law)) :
    |pathFlux (jet g r x J v m [] old) 1 0| ≤
      ∑ k ∈ range m, expect (μ k) (fun n => ∑ a, ‖(J k n).grad a‖)*
        (∑ l ∈ Ico k m, v l) := by
…

    Mentions: OAI.SignedDisk.DiskMoments.signedAverage, OAI.SignedDisk.SignedRuns.jet