OAI/Dynamics/ThreeTorus/Jitter.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Cumulative distribution, smooth quantile inverse, and positive smooth neutral jitter laws.

  1. def OAI.ThreeTorus.cumulative line 33

    Source documentation

    The manuscript's distribution function, without a normalization convention for non-probability inputs.

    def cumulative (ρ : ℝ → ℝ) (y : ℝ) : ℝ := ∫ x in Iic y, ρ x
  2. lemma OAI.ThreeTorus.cumulative_sub line 35
  3. lemma OAI.ThreeTorus.cumulative_eq_primitive line 39
  4. lemma OAI.ThreeTorus.hasDerivAt_cumulative line 44
  5. lemma OAI.ThreeTorus.contDiff_cumulative line 51
  6. lemma OAI.ThreeTorus.strictMono_cumulative line 61
  7. lemma OAI.ThreeTorus.cumulative_atBot line 65
  8. lemma OAI.ThreeTorus.cumulative_atTop line 69
  9. lemma OAI.ThreeTorus.cumulative_mem_Ioo line 75
  10. lemma OAI.ThreeTorus.range_cumulative line 85
  11. def OAI.ThreeTorus.quantile line 100

    Source documentation

    The inverse is only used on (0,1); its arbitrary values elsewhere are killed by a smooth compactly supported cutoff.

    def quantile (ρ : ℝ → ℝ) : ℝ → ℝ := invFun (cumulative ρ)

    Mentions: OAI.ThreeTorus.cumulative

  12. lemma OAI.ThreeTorus.cumulative_quantile line 102
  13. lemma OAI.ThreeTorus.quantile_cumulative line 110
  14. lemma OAI.ThreeTorus.contDiffAt_invFun_of_deriv_ne_zero line 115
  15. lemma OAI.ThreeTorus.contDiffOn_quantile line 135
  16. lemma OAI.ThreeTorus.hasDerivAt_quantile line 146
  17. def OAI.ThreeTorus.periodize line 158

    Source documentation

    Periodize by a locally finite sum. Unlike a raw fract expression this also makes smoothness at the identified endpoints explicit.

    def periodize (f : ℝ → ℝ) (x : ℝ) : ℝ := ∑ᶠ k : ℤ, f (x + k)
  18. lemma OAI.ThreeTorus.periodize_periodic line 160
  19. lemma OAI.ThreeTorus.contDiff_periodize line 165
  20. lemma OAI.ThreeTorus.periodize_eq_on_unit line 197
  21. lemma OAI.ThreeTorus.periodize_eq_fract line 211
  22. lemma OAI.ThreeTorus.contDiff_cutoff_quantile line 219
  23. structure OAI.ThreeTorus.LawCutoffs line 236

    Source documentation

    The two actual smooth cutoffs used by the manuscript's quantile construction.

    structure LawCutoffs (δ : ℝ) where
…
  24. def OAI.ThreeTorus.lawCutoffs line 250
  25. def OAI.ThreeTorus.lawJitter line 278
  26. def OAI.ThreeTorus.lawPsi line 281
  27. def OAI.ThreeTorus.lawDensity line 283
  28. lemma OAI.ThreeTorus.lawJitter_smooth line 286
  29. lemma OAI.ThreeTorus.lawJitter_eq_quantile line 293
  30. lemma OAI.ThreeTorus.lawJitter_deriv_pos line 300
  31. lemma OAI.ThreeTorus.lawPsi_smooth line 312
  32. lemma OAI.ThreeTorus.lawPsi_eq line 316
  33. lemma OAI.ThreeTorus.lawPsi_bounds line 323
  34. lemma OAI.ThreeTorus.lawDensity_smooth line 331
  35. lemma OAI.ThreeTorus.lawDensity_bounds line 336
  36. lemma OAI.ThreeTorus.lawDensity_compact line 344
  37. lemma OAI.ThreeTorus.lawDensity_integrable line 368
  38. lemma OAI.ThreeTorus.integral_lawDensity line 376
  39. lemma OAI.ThreeTorus.integral_cutoff_lower line 389
  40. lemma OAI.ThreeTorus.lawDensity_error line 409
  41. lemma OAI.ThreeTorus.lawDensity_pushforward line 425

    Source documentation

    Exact weighted pushforward, in a unit-interval representative of the circle. The cutoff is not renormalized.

    lemma lawDensity_pushforward {ρ : ℝ → ℝ} {δ : ℝ} (c : LawCutoffs δ)
    (hρ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ρ) (hi : Integrable ρ)
    (hp : ∀ y, 0 < ρ y) (hm : ∫ y, ρ y = 1) (hδ : 0 < δ) :
    Measure.map (lawJitter ρ c)
      ((volume.restrict (Ioo (0 : ℝ) 1)).withDensity (fun a => ENNReal.ofReal (c.ψ a^2))) =
      volume.withDensity (fun y => ENNReal.ofReal (lawDensity ρ c y)) := by
…

    Mentions: OAI.ThreeTorus.LawCutoffs, OAI.ThreeTorus.lawJitter, OAI.ThreeTorus.lawDensity

  42. lemma OAI.ThreeTorus.missing_cutoff_mass line 459
  43. theorem OAI.ThreeTorus.realize_jitter_law line 476

    Source documentation

    Source Lemma law-approx, using a compactly supported representative ψ of its circle cutoff on (0,1). Its smooth periodic extension is periodize ψ; periodize_eq_on_unit proves that this does not change the weighted measure. The output density is deliberately a subprobability, not normalized.

    theorem realize_jitter_law (ρ : ℝ → ℝ)
    (hρ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ρ) (hi : Integrable ρ)
    (hp : ∀ y, 0 < ρ y) (hm : ∫ y, ρ y = 1) {ε : ℝ} (hε : 0 < ε) :
    ∃ (δ : ℝ) (J ψ ρ' : ℝ → ℝ),
      0 < δ ∧ δ < 1/8 ∧ 2*δ < ε ∧
      ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J ∧ Periodic J 1 ∧
      (∀ a ∈ Ioo δ (1-δ), 0 < deriv J a) ∧
      ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ψ ∧ HasCompactSupport ψ ∧
      tsupport ψ ⊆ Ioo δ (1-δ) ∧ (∀ a, 0 ≤ ψ a ∧ ψ a ≤ 1) ∧
      ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ρ' ∧ HasCompactSupport ρ' ∧
      (∀ y, 0 ≤ ρ' y ∧ ρ' y ≤ ρ y) ∧ Integrable ρ' ∧
      Measure.map J ((volume.restrict (Ioo (0 : ℝ) 1)).withDensity
…
  44. def OAI.ThreeTorus.neutralJitterReal line 517

    Source documentation

    A bounded smooth periodic jitter that is exactly affine on the fixed large good arc. The cutoff and good arc do not depend on the slope.

    def neutralJitterReal {δ : ℝ} (c : LawCutoffs δ) (L β : ℝ) : ℝ → ℝ :=
…

    Mentions: OAI.ThreeTorus.LawCutoffs

  45. lemma OAI.ThreeTorus.neutralJitterReal_smooth line 520
  46. lemma OAI.ThreeTorus.neutralJitterReal_periodic line 525
  47. lemma OAI.ThreeTorus.neutralJitterReal_affine line 528
  48. lemma OAI.ThreeTorus.neutralJitterReal_deriv line 534
  49. def OAI.ThreeTorus.neutralJitter line 542
  50. lemma OAI.ThreeTorus.neutralJitter_coe line 545
  51. lemma OAI.ThreeTorus.continuous_neutralJitter line 548
  52. def OAI.ThreeTorus.neutralCircleCutoff line 554
  53. lemma OAI.ThreeTorus.neutralCircleCutoff_coe line 557
  54. lemma OAI.ThreeTorus.continuous_neutralCircleCutoff line 560
  55. lemma OAI.ThreeTorus.neutralCircleCutoff_bounds line 566
  56. lemma OAI.ThreeTorus.neutralCircleCutoff_error line 571