Runs.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SignedRuns.runEnvelope line 58
lemma OAI.SignedRuns.radius_antitone line 61
lemma OAI.SignedRuns.runEnvelope_attains line 67
lemma OAI.SignedRuns.runEnvelope_le_next line 75
lemma OAI.SignedRuns.runEnvelope_extension_bound line 83
lemma OAI.SignedRuns.runEnvelope_new_bound line 109
def OAI.SignedRuns.activeStart line 120
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
```
lemma OAI.SignedRuns.activeStart_le line 125

def OAI.SignedRuns.potential line 136

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.SignedRuns.runEnvelope, OAI.SignedRuns.activeStart

lemma OAI.SignedRuns.potential_increment line 145
theorem OAI.SignedRuns.potential_continuation_bound line 162

def OAI.SignedRuns.jet line 191

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.SignedRuns.potential

lemma OAI.SignedRuns.jet_terminalBound line 196
lemma OAI.SignedRuns.jet_controlled line 208

def OAI.SignedRuns.rewardCost line 226

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)

lemma OAI.SignedRuns.jet_cost line 230
lemma OAI.SignedRuns.expect_rewardCost line 245

theorem OAI.SignedRuns.run_signed_flux_bound line 261

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.DiskMoments.signedAverage, OAI.SignedRuns.jet

structure OAI.SignedRuns.Run line 284

def OAI.SignedRuns.closedRuns line 290

Source documentation

Completed runs, in reverse chronological order.

def closedRuns : List Label → List Run
  | [] => []
  | [_] => []
  | n::old::p => if n = old then closedRuns (old::p)
      else ⟨old,activeStart (old::p),p.length⟩::closedRuns (old::p)

Mentions: OAI.SignedRuns.Run, OAI.SignedRuns.activeStart

def OAI.SignedRuns.runs line 296
lemma OAI.SignedRuns.closedRuns_bounds line 300
lemma OAI.SignedRuns.runs_bounds line 315
lemma OAI.SignedRuns.runs_cover line 323
lemma OAI.SignedRuns.potential_eq_runs line 352
lemma OAI.SignedRuns.radius_in_bin line 366
lemma OAI.SignedRuns.runs_cover_radius line 377

lemma OAI.SignedRuns.winning_run line 390

Source documentation

Every history has an actually attaining winning run. No radius selection is differentiated.

lemma winning_run (g : ℂ → ℝ) (r : ℕ → ℝ) (hg : ContDiff ℝ 1 g)
    (hr : ∀ k, 0 < r k) (hstep : ∀ k, 2*r (k+1) = r k)
    (n : Label) (p : List Label) (x : ℂ) :
    ∃ a ∈ runs (n::p), ∃ t ∈ Icc (r a.last) (2*r a.first),
      runEnvelope g r 0 p.length x = signedAverage g x t ∧
      runEnvelope g r a.first a.last x = signedAverage g x t := by
…

Mentions: OAI.SignedRuns.runs, OAI.SignedRuns.runEnvelope

lemma OAI.FiniteLabels.Law.ext_mass line 411
def OAI.SignedAssembly.RowJet.ofLawAt line 424
Source documentation
The zero row-sum is obtained by differentiating the actual stochastic partition of unity, not postulated for the row derivatives.
```
def RowJet.ofLawAt (P : ℂ → Law ι) (x : ℂ)
    (hd : ∀ i, DifferentiableAt ℝ (fun y => P y i) x) : RowJet ι ℂ where
…
```
Mentions: OAI.SignedAssembly.RowJet
def OAI.ActualLabels.observation line 441
Source documentation
Observation time zero is the true initial spatial row. Subsequent times are the true state-dependent spatial switch rows.
```
def observation (h : ℂ → ℂ) (r : ℕ → ℝ) : ℕ → ℂ → Label → Law Label
  | 0,x,_ => initial h (r 0) x
  | k+1,x,n => row h (r (k+1)) x n
```
Mentions: OAI.ActualLabels.Label, OAI.ActualLabels.initial, OAI.ActualLabels.row
def OAI.ActualLabels.before line 445
lemma OAI.ActualLabels.before_move line 449
lemma OAI.ActualLabels.observation_lipschitz line 459
lemma OAI.ActualLabels.observation_ae_diff line 472
def OAI.ActualLabels.observationJet line 478

lemma OAI.ActualLabels.observationJet_cost line 485

Source documentation

The jet's expected absolute row derivative is exactly T_k/r_k from the physical spatial packing theorem.

lemma observationJet_cost (h : ℂ → ℂ) (r : ℕ → ℝ) (old : Label) (x : ℂ)
    (hd : ∀ k n j, DifferentiableAt ℝ (fun y => observation h r k y n j) x)
    (k : ℕ) (hr : 0 < r k) :
    expect (before h r old x k) (fun n => ∑ j, ‖(observationJet h r x hd k n).grad j‖) =
      derivativeCost h r x k/r k := by
…

Mentions: OAI.ActualLabels.Label, OAI.ActualLabels.observation, OAI.ActualLabels.before, OAI.ActualLabels.observationJet, OAI.ActualLabels.derivativeCost

def OAI.SignedRuns.weight line 505
lemma OAI.SignedRuns.weight_nonneg line 509
lemma OAI.SignedRuns.weight_le_one line 515
lemma OAI.SignedRuns.lipschitz_bounded_mul line 524
lemma OAI.SignedRuns.weight_lipschitz line 541
lemma OAI.SignedRuns.weight_diff line 555
lemma OAI.SignedRuns.gradient_weight_cons line 562

def OAI.SignedRuns.leafSum line 573

Source documentation

Unweighted finite sum over every possible terminal continuation.

def leafSum {E : Type*} [AddCommMonoid E] (f : List Label → E) : ℕ → List Label → E
  | 0,p => f p
  | d+1,p => ∑ n, leafSum f d (n::p)

lemma OAI.SignedRuns.flux_eq_weightedLeaves line 577

theorem OAI.SignedRuns.actual_signed_flux_bound line 597

Source documentation

The signed flux bound for derivatives of the actual spatial history weights, with the true initial row and forward marginal derivatives.

theorem actual_signed_flux_bound (g : ℂ → ℝ) (h : ℂ → ℂ) (r : ℕ → ℝ)
    (hg : ContDiff ℝ 1 g) (hr : ∀ k, 0 < r k) (hstep : ∀ k, 2*r (k+1) = r k)
    (old : Label) (x : ℂ)
    (hd : ∀ k n j, DifferentiableAt ℝ (fun y => observation h r k y n j) x)
    (v : ℕ → ℝ)
    (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 : ℕ) :
    |leafSum (fun q => inner ℝ (gradient (fun y => weight h r old y q) x) (potential g r x q)) m []| ≤
      ∑ k ∈ range m, (derivativeCost h r x k/r k)*(∑ l ∈ Ico k m, v l) := by
…

Mentions: OAI.DiskMoments.signedAverage, OAI.SignedRuns.leafSum, OAI.SignedRuns.weight, OAI.SignedRuns.potential

lemma OAI.SignedRuns.run_gradient_touching line 619
lemma OAI.SignedRuns.runs_ae_diff line 630
def OAI.SignedRuns.coneContribution line 641
lemma OAI.SignedRuns.coneContribution_nonneg line 644
theorem OAI.SignedRuns.run_master line 649
lemma OAI.DiskMoments.signedAverage_hasCompactSupport line 677