OAI/Analysis/SignedDisk/DiskMoments1.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.DiskMoments.signedAverage_hasCompactSupport line 31
2. def OAI.SignedDisk.SignedRuns.Regular line 47
3. lemma OAI.SignedDisk.SignedRuns.regular_zero line 49
4. lemma OAI.SignedDisk.SignedRuns.regular_add line 52
5. lemma OAI.SignedDisk.SignedRuns.regular_scalar line 58
6. lemma OAI.SignedDisk.SignedRuns.regular_listSum line 65
7. lemma OAI.SignedDisk.SignedRuns.runTerm_regular line 72
8. theorem OAI.SignedDisk.SignedRuns.potential_regular line 87

   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.SignedDisk.SignedRuns.Regular, OAI.SignedDisk.SignedRuns.potential

9. def OAI.SignedDisk.SignedRuns.divergence line 99
10. lemma OAI.SignedDisk.SignedRuns.inner_coordinates line 102
11. lemma OAI.SignedDisk.SignedRuns.gradient_aestronglyMeasurable line 111
12. lemma OAI.SignedDisk.SignedRuns.gradient_norm_le line 115
13. lemma OAI.SignedDisk.SignedRuns.integrable_fderiv_apply line 120
14. lemma OAI.SignedDisk.SignedRuns.integrable_gradient_mul line 128
15. lemma OAI.SignedDisk.SignedRuns.regular_integrable line 134
16. lemma OAI.SignedDisk.SignedRuns.weighted_divergence_integrable line 138
17. lemma OAI.SignedDisk.SignedRuns.potential_flux_integrable line 148
18. theorem OAI.SignedDisk.SignedRuns.vector_weighted_ibp line 159

    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.SignedDisk.SignedRuns.Regular, OAI.SignedDisk.SignedRuns.divergence

19. lemma OAI.SignedDisk.SignedRuns.leafSum_add line 184
20. lemma OAI.SignedDisk.SignedRuns.leafSum_mul_const line 190
21. lemma OAI.SignedDisk.SignedRuns.leafSum_const_mul line 196
22. lemma OAI.SignedDisk.SignedRuns.leafSum_neg line 200
23. lemma OAI.SignedDisk.SignedRuns.leafSum_mono line 204
24. lemma OAI.SignedDisk.SignedRuns.leafSum_congr line 217
25. lemma OAI.SignedDisk.SignedRuns.leafSum_weight line 222
26. lemma OAI.SignedDisk.SignedRuns.leafSum_integrable line 229
27. lemma OAI.SignedDisk.SignedRuns.integral_leafSum line 235
28. theorem OAI.SignedDisk.SignedRuns.history_weighted_ibp line 245
29. theorem OAI.SignedDisk.SignedRuns.expected_run_master line 271

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

30. lemma OAI.SignedDisk.SignedRuns.divergence_add line 299
31. lemma OAI.SignedDisk.SignedRuns.divergence_scalar line 311
32. lemma OAI.SignedDisk.SignedRuns.listSum_diff line 321
33. lemma OAI.SignedDisk.SignedRuns.divergence_listSum line 329
34. lemma OAI.SignedDisk.SignedRuns.average_diff line 339
35. lemma OAI.SignedDisk.SignedRuns.potential_divergence line 346

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

36. lemma OAI.SignedDisk.SignedRuns.radius_in_run_bin line 370
37. lemma OAI.SignedDisk.SignedRuns.attaining_endpoint line 378
38. lemma OAI.SignedDisk.SignedRuns.attaining_interior line 392
39. def OAI.SignedDisk.SignedRuns.unfavorable line 406
40. lemma OAI.SignedDisk.SignedRuns.unfavorable_nonneg line 409
41. lemma OAI.SignedDisk.SignedRuns.unfavorable_le_norm line 412
42. lemma OAI.SignedDisk.SignedRuns.run_unfavorable_bound line 425

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