OAI/Analysis/SignedDisk/SignedRuns2.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.SignedRuns.leafSum_succ_last line 33
2. lemma OAI.SignedDisk.SignedRuns.leafSum_sum line 43
3. lemma OAI.SignedDisk.SignedRuns.leafSum_headLaw line 51

   Source documentation

   The exact head law obtained from the genuine finite-history products.

   lemma leafSum_headLaw (h : ℂ → ℂ) (r : ℕ → ℝ) (old : Label) (x : ℂ)
       (m : ℕ) (F : Label → ℝ) :
       leafSum (fun q => weight h r old x q*F (q.headD old)) m [] =
         expect (before h r old x m) F := by
   …

   Mentions: OAI.SignedDisk.SignedRuns.leafSum, OAI.SignedDisk.SignedRuns.weight

4. def OAI.SignedDisk.SignedRuns.pathReward line 75

   Source documentation

   Additive reward along a reversed history, with its true previous state.

   def pathReward (old : Label) (A : ℕ → Label → Label → ℝ) : List Label → ℝ
     | [] => 0
     | n::p => pathReward old A p+A p.length (p.headD old) n

5. lemma OAI.SignedDisk.SignedRuns.leafSum_pathReward line 79
6. lemma OAI.SignedDisk.SignedRuns.pathReward_add line 107
7. lemma OAI.SignedDisk.SignedRuns.pathReward_nonneg line 114
8. lemma OAI.SignedDisk.SignedRuns.run_span_sum line 122
9. def OAI.SignedDisk.SignedRuns.startReward line 149
10. def OAI.SignedDisk.SignedRuns.boundaryReward line 153
11. lemma OAI.SignedDisk.SignedRuns.run_start_sum line 157
12. lemma OAI.SignedDisk.SignedRuns.run_boundary_sum line 176
13. lemma OAI.SignedDisk.SignedRuns.startReward_nonneg line 193
14. lemma OAI.SignedDisk.SignedRuns.boundaryReward_nonneg line 199
15. lemma OAI.SignedDisk.ActualLabels.row_change_le_rate line 210
16. lemma OAI.SignedDisk.ActualLabels.observation_startReward_le line 218
17. def OAI.SignedDisk.ActualLabels.boundaryCost line 239
18. lemma OAI.SignedDisk.ActualLabels.boundaryCost_nonneg line 242
19. lemma OAI.SignedDisk.ActualLabels.observation_boundaryReward_le line 250
20. lemma OAI.SignedDisk.ActualLabels.boundary_reward_sum line 269
21. lemma OAI.SignedDisk.SignedRuns.expected_start_sum_bound line 299
22. lemma OAI.SignedDisk.SignedRuns.expected_boundary_sum_bound line 307
23. lemma OAI.SignedDisk.SignedRuns.expected_span_sum line 325
24. def OAI.SignedDisk.PhysicalCells.gridIndex line 341
25. lemma OAI.SignedDisk.PhysicalCells.toUnit_point_re line 343
26. lemma OAI.SignedDisk.PhysicalCells.toUnit_point_im line 348
27. lemma OAI.SignedDisk.PhysicalCells.mem_index_cell line 353
28. lemma OAI.SignedDisk.PhysicalCells.cells_cover line 363
29. lemma OAI.SignedDisk.PhysicalCells.mem_cell_box line 368
30. lemma OAI.SignedDisk.PhysicalCells.cell_subset_root_neighborhood line 381
31. lemma OAI.SignedDisk.PhysicalCells.lintegral_le_cells line 394
32. lemma OAI.SignedDisk.PhysicalCells.tsum_ofReal_le line 399
33. lemma OAI.SignedDisk.PhysicalCells.integral_cell_budget line 410

    Source documentation

    Global integration over the actual full lattice. The budget is tested on arbitrary finite sets, so neither support cutoffs nor omitted cells enter.

    lemma integral_cell_budget {r : ℝ} (hr : 0 < r) (F : ℂ → ℝ≥0∞)
        (B : (ℤ × ℤ) → ℝ) (hB : ∀ p, 0 ≤ B p) (A : ℝ)
        (hcell : ∀ p, (∫⁻ y in cell (point r p) r, F y) ≤ ENNReal.ofReal (B p))
        (hbudget : ∀ s : Finset (ℤ × ℤ), ∑ p ∈ s, B p ≤ A) :
        (∫⁻ y, F y) ≤ ENNReal.ofReal A :=
    …

    Mentions: OAI.SignedDisk.PhysicalCells.cell