OAI/Analysis/SignedDisk/CommonPrices2.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.CommonPrices.cellRoots_budget line 33
2. lemma OAI.SignedDisk.CommonPrices.badPrice_nonneg line 50
3. lemma OAI.SignedDisk.CommonPrices.badPrice_le_rootMass line 53
4. lemma OAI.SignedDisk.ActualLabels.marginal_localSup_nonneg line 62
5. lemma OAI.SignedDisk.ActualLabels.marginal_localSup_le_one line 66
6. lemma OAI.SignedDisk.ActualLabels.marginal_localSup_bad_zero line 70
7. lemma OAI.SignedDisk.ActualLabels.marginal_badPrice_bound line 87

   Source documentation

   The actual bad-root charge is paid by geometric energy, not a separately assumed probability budget.

   lemma marginal_badPrice_bound {N : ℕ} (h : ℂ → ℂ) (r : ℕ → ℝ) (base : ℝ)
       (k j : ℕ) (hr : 0 < r k) (hrj : r k = scale base j) (p : ℤ × ℤ) (n : Label) :
       localSup (fun x => marginal h r k x n) (r k) p*badPrice h base j (cellRoots N p) n ≤
         1000000*∑ q ∈ cellRoots N p, scalarMass h (r k) q*energy h (r k) q := by
   …

   Mentions: OAI.SignedDisk.ActualLabels.Label, OAI.SignedDisk.ActualLabels.marginal

8. def OAI.SignedDisk.PhysicalCells.patch line 123

   Source documentation

   Measurable full-lattice patch; no choice of maximizing radius occurs.

   def patch (r : ℝ) (F : (ℤ × ℤ) → ℂ → ℝ≥0∞) (x : ℂ) : ℝ≥0∞ :=
   …

9. lemma OAI.SignedDisk.PhysicalCells.patch_measurable line 126
10. lemma OAI.SignedDisk.PhysicalCells.le_patch line 130
11. lemma OAI.SignedDisk.PhysicalCells.lintegral_patch line 135
12. lemma OAI.SignedDisk.PhysicalCells.lintegral_patch_budget line 141
13. lemma OAI.SignedDisk.PhysicalCells.patch_finite line 149
14. lemma OAI.SignedDisk.PhysicalCells.patch_integrable line 155
15. lemma OAI.SignedDisk.PhysicalCells.real_le_patch line 161
16. lemma OAI.SignedDisk.PhysicalCells.weighted_patch_bound line 170

    Source documentation

    Take the cell supremum of a weight only after the local price has been proved. This bounds all three spatial budgets by the corresponding local prices.

    lemma weighted_patch_bound (r : ℝ) (F : (ℤ × ℤ) → ℂ → ℝ≥0∞) (hF : ∀ p, Measurable (F p))
        (W : ℂ → ℝ≥0∞) (hW : Measurable W) (A B : (ℤ × ℤ) → ℝ)
        (hA : ∀ p, 0 ≤ A p) (_hB : ∀ p, 0 ≤ B p)
        (hcell : ∀ p, (∫⁻ x in cell (point r p) r, F p x) ≤ ENNReal.ofReal (B p))
        (hWB : ∀ p x, x ∈ cell (point r p) r → W x ≤ ENNReal.ofReal (A p)) :
        (∫⁻ x, W x*patch r F x) ≤ ∑' p, ENNReal.ofReal (A p*B p) := by
    …

    Mentions: OAI.SignedDisk.PhysicalCells.cell, OAI.SignedDisk.PhysicalCells.patch

17. def OAI.SignedDisk.ActualLabels.geometricRadii line 200

    Source documentation

    Global geometric extension of the finite descending radius grid.

    def geometricRadii (base : ℝ) (m : ℕ) (k : ℕ) : ℝ := scale base m/(2:ℝ)^k

18. lemma OAI.SignedDisk.ActualLabels.geometricRadii_pos line 201
19. lemma OAI.SignedDisk.ActualLabels.geometricRadii_step line 203
20. lemma OAI.SignedDisk.ActualLabels.geometricRadii_eq line 208
21. lemma OAI.SignedDisk.ActualLabels.marginal_congr line 216
22. lemma OAI.SignedDisk.ActualLabels.switchCost_congr line 223
23. lemma OAI.SignedDisk.ActualLabels.derivativeCost_congr line 230
24. lemma OAI.SignedDisk.ActualLabels.cellCost_congr line 237
25. lemma OAI.SignedDisk.SignedRuns.run_cone_bound line 260
26. theorem OAI.SignedDisk.SignedRuns.pointwise_signed_master line 291

    Source documentation

    Complete pointwise signed assembly, still retaining the divergence term. The remaining terms are exactly the direct directional and boundary costs.

    theorem pointwise_signed_master {g : ℂ → ℝ} (h : ℂ → ℂ) {r : ℕ → ℝ}
        (hg : ContDiff ℝ 1 g) (hc : HasCompactSupport g)
        (hr : ∀ k, 0 < r k) (hstep : ∀ k, 2*r (k+1) = r k)
        (H : ℕ → Label → ℝ) (J : ℕ → ℝ) (hH : ∀ k n, 0 ≤ H k n) (hJ : ∀ k, 0 ≤ J k)
        (old : Label) (m : ℕ) (x : ℂ)
        (hd : ∀ i j, i ≤ j → DifferentiableAt ℝ (runEnvelope g r i j) x)
        (hinterior : ∀ k n t, PhysicalNeighborhoodRadius g (r k) x t →
          unfavorable n (gradient (fun y => signedAverage g y t) x) ≤ H k n)
        (hend : ∀ k t, PhysicalEndpointRadius g (r k) x t →
          ‖gradient (fun y => signedAverage g y t) x‖ ≤ J k) :
        ‖gradient (runEnvelope g r 0 m) x‖ ≤ 12*(
          leafSum (fun q => weight h r old x q*divergence (fun y => potential g r y q) x) (m+1) []+
    …

    Mentions: OAI.SignedDisk.SignedRuns.runEnvelope, OAI.SignedDisk.SignedRuns.unfavorable, OAI.SignedDisk.SignedRuns.leafSum, OAI.SignedDisk.SignedRuns.weight, OAI.SignedDisk.SignedRuns.divergence, OAI.SignedDisk.SignedRuns.potential

27. lemma OAI.SignedDisk.PhysicalCells.center_mem_cell line 340
28. def OAI.SignedDisk.PhysicalCells.cellSup line 342
29. lemma OAI.SignedDisk.PhysicalCells.cellSup_le line 344
30. lemma OAI.SignedDisk.PhysicalCells.le_cellSup line 349
31. lemma OAI.SignedDisk.PhysicalCells.cellSup_nonneg line 352
32. def OAI.SignedDisk.ActualLabels.pointCost line 360
33. def OAI.SignedDisk.ActualLabels.costLimit line 363
34. lemma OAI.SignedDisk.ActualLabels.costLimit_pos line 364
35. lemma OAI.SignedDisk.ActualLabels.pointCost_nonneg line 365
36. lemma OAI.SignedDisk.ActualLabels.pointCost_le line 368
37. lemma OAI.SignedDisk.ActualLabels.pointCost_le_cellCost line 377
38. lemma OAI.SignedDisk.ActualLabels.cellSup_pointCost_le line 388
39. lemma OAI.SignedDisk.ActualLabels.cellSup_pointCost_nonneg line 395
40. lemma OAI.SignedDisk.ActualLabels.cellSup_pointCost_uniform line 398
41. lemma OAI.SignedDisk.ActualLabels.pointCost_cell_budget line 402