OAI/Analysis/DiskMaximal/RunCancellation.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedRuns.Regular line 57
2. lemma OAI.SignedRuns.regular_zero line 59
3. lemma OAI.SignedRuns.regular_add line 62
4. lemma OAI.SignedRuns.regular_scalar line 68
5. lemma OAI.SignedRuns.regular_listSum line 75
6. lemma OAI.SignedRuns.runTerm_regular line 82
7. theorem OAI.SignedRuns.potential_regular line 97

   Source documentation

   Every exact history potential is compactly supported and Lipschitz, as needed for signed weighted integration by parts.

   theorem potential_regular {g : ℂ → ℝ} {r : ℕ → ℝ} (hg : ContDiff ℝ 1 g)
       (hgc : HasCompactSupport g) (hr : ∀ k, 0 < r k) (hstep : ∀ k, 2*r (k+1) = r k)
       (p : List Label) : Regular (fun x => potential g r x p) := by
   …

   Mentions: OAI.SignedRuns.Regular, OAI.SignedRuns.potential

8. def OAI.SignedRuns.divergence line 111
9. lemma OAI.SignedRuns.inner_coordinates line 114
10. lemma OAI.SignedRuns.gradient_aestronglyMeasurable line 123
11. lemma OAI.SignedRuns.gradient_norm_le line 127
12. lemma OAI.SignedRuns.integrable_fderiv_apply line 132
13. lemma OAI.SignedRuns.integrable_gradient_mul line 140
14. lemma OAI.SignedRuns.regular_integrable line 146
15. lemma OAI.SignedRuns.weighted_divergence_integrable line 150
16. lemma OAI.SignedRuns.potential_flux_integrable line 160
17. theorem OAI.SignedRuns.vector_weighted_ibp line 171

    Source documentation

    Weighted vector integration by parts for the actual class of compact Lipschitz path potentials and bounded Lipschitz spatial history weights.

    theorem vector_weighted_ibp {w : ℂ → ℝ} {K : ℝ≥0} (hw : LipschitzWith K w)
        (hb : ∀ x, ‖w x‖ ≤ 1) {V : ℂ → ℂ} (hV : Regular V) :
        (∫ x, w x*divergence V x) = -∫ x, inner ℝ (gradient w x) (V x) := by
    …

    Mentions: OAI.SignedRuns.Regular, OAI.SignedRuns.divergence

18. lemma OAI.SignedRuns.leafSum_add line 198
19. lemma OAI.SignedRuns.leafSum_mul_const line 204
20. lemma OAI.SignedRuns.leafSum_const_mul line 210
21. lemma OAI.SignedRuns.leafSum_neg line 214
22. lemma OAI.SignedRuns.leafSum_mono line 218
23. lemma OAI.SignedRuns.leafSum_congr line 231
24. lemma OAI.SignedRuns.leafSum_weight line 236
25. lemma OAI.SignedRuns.leafSum_integrable line 243
26. lemma OAI.SignedRuns.integral_leafSum line 249
27. theorem OAI.SignedRuns.history_weighted_ibp line 259
28. theorem OAI.SignedRuns.expected_run_master line 285

    Source documentation

    Averaging preserves the complete signed run-master inequality; finite history weights sum to one at every observation point.

    theorem expected_run_master (g : ℂ → ℝ) (h : ℂ → ℂ) (r : ℕ → ℝ)
        (hg : ContDiff ℝ 1 g) (hc : HasCompactSupport g) (hr : ∀ k, 0 < r k)
        (hstep : ∀ k, 2*r (k+1) = r k) (old : Label) (m : ℕ) (x : ℂ)
        (hd : ∀ i j, i ≤ j → DifferentiableAt ℝ (runEnvelope g r i j) x) :
        ‖gradient (runEnvelope g r 0 m) x‖ ≤
          12*leafSum (fun q => weight h r old x q*((runs q).map fun a => coneContribution a.dir
            (gradient (runEnvelope g r a.first a.last) x)).sum) (m+1) [] := by
    …

    Mentions: OAI.SignedRuns.runEnvelope, OAI.SignedRuns.leafSum, OAI.SignedRuns.weight, OAI.SignedRuns.runs, OAI.SignedRuns.coneContribution

29. lemma OAI.SignedRuns.divergence_add line 315
30. lemma OAI.SignedRuns.divergence_scalar line 327
31. lemma OAI.SignedRuns.listSum_diff line 337
32. lemma OAI.SignedRuns.divergence_listSum line 345
33. lemma OAI.SignedRuns.average_diff line 355
34. lemma OAI.SignedRuns.potential_divergence line 362

    Source documentation

    The divergence of the exact path potential is the complete signed sum of run gradients, with precisely the starting-baseline gradients removed.

    lemma potential_divergence {g : ℂ → ℝ} {r : ℕ → ℝ} (hg : ContDiff ℝ 1 g)
        (hgc : HasCompactSupport g) (hr : ∀ k, 0 < r k) (p : List Label) (x : ℂ)
        (hd : ∀ i j, i ≤ j → DifferentiableAt ℝ (runEnvelope g r i j) x) :
        divergence (fun y => potential g r y p) x =
          ((runs p).map fun a => inner ℝ (a.dir:ℂ)
            (gradient (runEnvelope g r a.first a.last) x-gradient (fun y => signedAverage g y (r a.first)) x)).sum := by
    …

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

35. lemma OAI.SignedRuns.radius_in_run_bin line 388
36. lemma OAI.SignedRuns.attaining_endpoint line 396
37. lemma OAI.SignedRuns.attaining_interior line 410
38. def OAI.SignedRuns.unfavorable line 424
39. lemma OAI.SignedRuns.unfavorable_nonneg line 427
40. lemma OAI.SignedRuns.unfavorable_le_norm line 430
41. lemma OAI.SignedRuns.run_unfavorable_bound line 443

    Source documentation

    The exact unfavorable run term is charged either to one interior bin or one of its two end bins; padding by nonnegative costs permits summing runs.

    lemma run_unfavorable_bound {g : ℂ → ℝ} {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)
        (x : ℂ) (n : Label) {i j : ℕ} (hij : i ≤ j)
        (hd : DifferentiableAt ℝ (runEnvelope g r i j) x)
        (hinterior : ∀ k 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) :
        unfavorable n (gradient (runEnvelope g r i j) x) ≤
          (∑ k ∈ Icc i j, H k n)+2*(J i+J j) := by
    …

    Mentions: OAI.SignedRuns.runEnvelope, OAI.SignedRuns.unfavorable

42. lemma OAI.SignedRuns.leafSum_succ_last line 479
43. lemma OAI.SignedRuns.leafSum_sum line 489
44. lemma OAI.SignedRuns.leafSum_headLaw line 497

    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.SignedRuns.leafSum, OAI.SignedRuns.weight

45. def OAI.SignedRuns.pathReward line 521

    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

46. lemma OAI.SignedRuns.leafSum_pathReward line 525
47. lemma OAI.SignedRuns.pathReward_add line 553
48. lemma OAI.SignedRuns.pathReward_nonneg line 560
49. lemma OAI.SignedRuns.run_span_sum line 571
50. def OAI.SignedRuns.startReward line 598
51. def OAI.SignedRuns.boundaryReward line 602
52. lemma OAI.SignedRuns.run_start_sum line 606
53. lemma OAI.SignedRuns.run_boundary_sum line 625
54. lemma OAI.SignedRuns.startReward_nonneg line 642
55. lemma OAI.SignedRuns.boundaryReward_nonneg line 648