OAI/Analysis/SignedDisk/CommonPrices1.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedDisk.CommonPrices.cellRoots line 33
2. lemma OAI.SignedDisk.CommonPrices.cellPrice_spatial line 36
3. theorem OAI.SignedDisk.CommonPrices.cellPrice_budget line 58

   Source documentation

   The common geometric price has a genuine uniform spatial-and-scale budget, including every desired finite set of observation cells.

   theorem cellPrice_budget {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) (m : ℕ) (P : ℕ → Finset (ℤ × ℤ)) :
       (∑ k ∈ range (m+1), ∑ p ∈ P k, cellPrice N r h k (cellRoots N p)) ≤
         1681*((fixedPalette.labels.card:ℝ)*2/(1-rho))*(∫ y, ‖h y‖) := by
   …

   Mentions: OAI.SignedDisk.CommonPrices.cellPrice, OAI.SignedDisk.CommonPrices.cellRoots, OAI.SignedDisk.CommonPrices.rho

4. lemma OAI.SignedDisk.ActualMarkTrees.nodeCharge_scale line 78
5. def OAI.SignedDisk.ActualMarkTrees.spatialCharge line 98
6. lemma OAI.SignedDisk.ActualMarkTrees.spatialCharge_cons line 101
7. lemma OAI.SignedDisk.ActualMarkTrees.sum_nodeCharge line 105
8. lemma OAI.SignedDisk.ActualMarkTrees.sum_energyCharge line 134
9. def OAI.SignedDisk.ActualMarkTrees.particleSwitches line 152

   Source documentation

   Particle observations use the prescribed terminal vertex, not a hat-density surrogate. This is the frozen spatial location carried throughout the process.

   def particleSwitches {N : ℕ} (h : ℂ → ℂ) (r : ℝ) (k : ℕ) (q : Grid N)
       (p : List (Grid N)) (b : ℕ) : ℝ :=
   …

10. theorem OAI.SignedDisk.ActualMarkTrees.particle_switch_bound line 156
11. theorem OAI.SignedDisk.ActualMarkTrees.forest_switch_budget line 177

    Source documentation

    The switch budget for the actual finite spatial forest, with every birth population included and frozen terminal positions observed.

    theorem forest_switch_budget {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, particleEval (tree (fun q => vectorMass h r q) k 1 q)
          (particleSwitches h r k q)) ≤
          (2560004+2000000*(576*(4097:ℝ)^2))*(∫ y, ‖h y‖) := by
    …

    Mentions: OAI.SignedDisk.ActualMarkTrees.tree, OAI.SignedDisk.ActualMarkTrees.particleSwitches

12. lemma OAI.SignedDisk.FiniteLabels.expect_const line 196
13. lemma OAI.SignedDisk.FiniteLabels.expect_mul line 198
14. lemma OAI.SignedDisk.FiniteLabels.expect_mono line 201
15. lemma OAI.SignedDisk.FiniteLabels.expect_le_const line 203
16. lemma OAI.SignedDisk.FiniteLabels.expect_compare line 205
17. def OAI.SignedDisk.ActualLabels.comparisonConstant line 216
18. lemma OAI.SignedDisk.ActualLabels.comparisonConstant_ge line 217
19. lemma OAI.SignedDisk.ActualLabels.comparisonConstant_pos line 220
20. lemma OAI.SignedDisk.ActualLabels.comparisonConstant_one line 221
21. def OAI.SignedDisk.ActualLabels.rowDerivative line 223
22. def OAI.SignedDisk.ActualLabels.derivativeCost line 225
23. lemma OAI.SignedDisk.ActualLabels.rowDerivative_nonneg line 229
24. lemma OAI.SignedDisk.ActualLabels.rowDerivative_uniform line 231
25. lemma OAI.SignedDisk.ActualLabels.initial_distance line 239
26. lemma OAI.SignedDisk.ActualLabels.derivativeCost_uniform line 250
27. lemma OAI.SignedDisk.ActualLabels.rate_local line 261
28. lemma OAI.SignedDisk.ActualLabels.row_local_distance line 273
29. lemma OAI.SignedDisk.ActualLabels.row_local_derivative line 294
30. lemma OAI.SignedDisk.AffineDensities.gradient_affine line 313
31. lemma OAI.SignedDisk.DyadicHats.vector_partition_grid line 328
32. lemma OAI.SignedDisk.CommonPrices.hat_mem_cellRoots line 345
33. lemma OAI.SignedDisk.CommonPrices.cell_partition line 362
34. lemma OAI.SignedDisk.CommonPrices.cell_decomposition_gradient line 374
35. theorem OAI.SignedDisk.CommonPrices.directional_cell_price line 388

    Source documentation

    The hard directional local price, instantiated with the actual common-price cone decomposition on the actual neighboring grid roots.

    theorem directional_cell_price : ∃ C : ℝ, 0 < C ∧
        ∀ {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R) (hN : R/r+1 ≤ (N:ℝ))
        {g : ℂ → ℝ}, ContDiff ℝ 1 g → Integrable (gradient g) →
        (∀ y, gradient g y ≠ 0 → ‖y‖ ≤ R) → ∀ (k : ℕ) (p : ℤ × ℤ)
        {n : ℂ}, n ∈ fixedPalette.labels → ∀ {s : ℝ}, (s = 1 ∨ s = -1) →
        ∀ Q : Set ℂ, volume Q ≤ ENNReal.ofReal 1 →
        ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
          (∫⁻ X in Q, F X) ≤ ENNReal.ofReal (C*(scale r k)⁻¹*
            (badPrice (gradient g) r k (cellRoots N p) n+cellPrice N r (gradient g) k (cellRoots N p))) ∧
          ∀ X, ‖X‖ ≤ 2 → ∀ t,
            NeighborhoodRadius (fun Y => g (point (scale r k) p+scale r k • Y)) X t →
            ENNReal.ofReal (max 0 (-inner ℝ (axis n s)
    …

    Mentions: OAI.SignedDisk.CommonPrices.badPrice, OAI.SignedDisk.CommonPrices.cellRoots, OAI.SignedDisk.CommonPrices.cellPrice