OAI/Analysis/SignedDisk/SignedRuns1.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SignedDisk.SignedRuns.Run line 33
2. def OAI.SignedDisk.SignedRuns.closedRuns line 39

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

3. def OAI.SignedDisk.SignedRuns.runs line 45
4. lemma OAI.SignedDisk.SignedRuns.closedRuns_bounds line 49
5. lemma OAI.SignedDisk.SignedRuns.runs_bounds line 64
6. lemma OAI.SignedDisk.SignedRuns.runs_cover line 72
7. lemma OAI.SignedDisk.SignedRuns.potential_eq_runs line 101
8. lemma OAI.SignedDisk.SignedRuns.radius_in_bin line 115
9. lemma OAI.SignedDisk.SignedRuns.runs_cover_radius line 126
10. lemma OAI.SignedDisk.SignedRuns.winning_run line 139

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

11. lemma OAI.SignedDisk.FiniteLabels.Law.ext_mass line 160
12. def OAI.SignedDisk.SignedAssembly.RowJet.ofLawAt line 173

    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.SignedDisk.SignedAssembly.RowJet

13. def OAI.SignedDisk.ActualLabels.observation line 190

    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.SignedDisk.ActualLabels.Label, OAI.SignedDisk.ActualLabels.initial, OAI.SignedDisk.ActualLabels.row

14. def OAI.SignedDisk.ActualLabels.before line 194
15. lemma OAI.SignedDisk.ActualLabels.before_move line 198
16. lemma OAI.SignedDisk.ActualLabels.observation_lipschitz line 208
17. lemma OAI.SignedDisk.ActualLabels.observation_ae_diff line 221
18. def OAI.SignedDisk.ActualLabels.observationJet line 227
19. lemma OAI.SignedDisk.ActualLabels.observationJet_cost line 234

    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.SignedDisk.ActualLabels.Label, OAI.SignedDisk.ActualLabels.observation, OAI.SignedDisk.ActualLabels.before, OAI.SignedDisk.ActualLabels.observationJet, OAI.SignedDisk.ActualLabels.derivativeCost

20. def OAI.SignedDisk.SignedRuns.weight line 254
21. lemma OAI.SignedDisk.SignedRuns.weight_nonneg line 258
22. lemma OAI.SignedDisk.SignedRuns.weight_le_one line 264
23. lemma OAI.SignedDisk.SignedRuns.lipschitz_bounded_mul line 273
24. lemma OAI.SignedDisk.SignedRuns.weight_lipschitz line 290
25. lemma OAI.SignedDisk.SignedRuns.weight_diff line 304
26. lemma OAI.SignedDisk.SignedRuns.gradient_weight_cons line 311
27. def OAI.SignedDisk.SignedRuns.leafSum line 321
28. lemma OAI.SignedDisk.SignedRuns.flux_eq_weightedLeaves line 325
29. theorem OAI.SignedDisk.SignedRuns.actual_signed_flux_bound line 345

    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.SignedDisk.DiskMoments.signedAverage, OAI.SignedDisk.SignedRuns.leafSum, OAI.SignedDisk.SignedRuns.weight, OAI.SignedDisk.SignedRuns.potential

30. lemma OAI.SignedDisk.SignedRuns.run_gradient_touching line 365
31. lemma OAI.SignedDisk.SignedRuns.runs_ae_diff line 376
32. def OAI.SignedDisk.SignedRuns.coneContribution line 387
33. lemma OAI.SignedDisk.SignedRuns.coneContribution_nonneg line 390
34. theorem OAI.SignedDisk.SignedRuns.run_master line 395