OAI/Geometry/PinnedDistances/RandomGrids.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPinned.Grid.bin line 22
  2. def OAI.WeakPinned.Grid.shares line 23
  3. lemma OAI.WeakPinned.Grid.bin_period line 25
  4. lemma OAI.WeakPinned.Grid.shares_period line 31
  5. lemma OAI.WeakPinned.Grid.shares_symm line 36
  6. lemma OAI.WeakPinned.Grid.measurable_shares line 39
  7. lemma OAI.WeakPinned.Grid.bin_small_shift line 45
  8. lemma OAI.WeakPinned.Grid.shares_small_shift line 56
  9. lemma OAI.WeakPinned.Grid.shares_integral line 76
  10. lemma OAI.WeakPinned.Grid.shares_integrableOn line 104
  11. lemma OAI.WeakPinned.Grid.square_shares_integral line 111

    Source documentation

    Independent uniform shifts in the two axes give a product of overlap lengths. This integral is unnormalized planar Lebesgue mass.

    lemma square_shares_integral {l : ℝ} (hl : 0 < l) (x y : ℝ × ℝ) :
    (∫ s₁ : ℝ in Set.Ioc 0 l, ∫ s₂ : ℝ in Set.Ioc 0 l,
      shares l s₁ x.1 y.1 * shares l s₂ x.2 y.2) =
      max 0 (l-|x.1-y.1|) * max 0 (l-|x.2-y.2|) := by
…

    Mentions: OAI.WeakPinned.Grid.shares

  12. lemma OAI.WeakPinned.Grid.shares_gap line 118
  13. lemma OAI.WeakPinned.Grid.bin_double line 140
  14. lemma OAI.WeakPinned.Grid.nested_bins line 148
  15. def OAI.WeakPinned.Grid.uniformInterval line 153

    Source documentation

    Normalized Lebesgue measure on a half-open interval of positive length.

    def uniformInterval (l : ℝ) : Measure ℝ :=
…
  16. lemma OAI.WeakPinned.Grid.uniformInterval_probability line 156
  17. instance OAI.WeakPinned.Grid.uniformInterval_finite line 163
  18. lemma OAI.WeakPinned.Grid.translate_restrict_Ioc line 172
  19. def OAI.WeakPinned.Grid.binaryStep line 186

    Source documentation

    A fair binary step of length l.

    def binaryStep (l : ℝ) : Measure ℝ := bernoulliMeasure 0 l ⟨1/2, by norm_num⟩
  20. instance OAI.WeakPinned.Grid.binaryStep_probability line 188
  21. lemma OAI.WeakPinned.Grid.binaryStep_eq line 192
  22. lemma OAI.WeakPinned.Grid.uniform_double line 207
  23. def OAI.WeakPinned.Grid.incrementLaw line 224

    Source documentation

    One initial uniform shift followed by independent fair coarsening bits, before introducing phase and orientation.

    def incrementLaw : ℕ → Measure ℝ
  | 0 => uniformInterval 1
  | n+1 => binaryStep (2^n)

    Mentions: OAI.WeakPinned.Grid.uniformInterval, OAI.WeakPinned.Grid.binaryStep

  24. instance OAI.WeakPinned.Grid.incrementLaw_probability line 228
  25. def OAI.WeakPinned.Grid.axisLaw line 233
  26. instance OAI.WeakPinned.Grid.axisLaw_probability line 234
  27. def OAI.WeakPinned.Grid.shift line 238
  28. lemma OAI.WeakPinned.Grid.measurable_shift line 240
  29. lemma OAI.WeakPinned.Grid.shift_zero line 243
  30. lemma OAI.WeakPinned.Grid.shift_succ line 244
  31. lemma OAI.WeakPinned.Grid.map_shift line 247
  32. lemma OAI.WeakPinned.Grid.integral_uniform_shares line 271
  33. lemma OAI.WeakPinned.Grid.integral_shift_shares line 279
  34. lemma OAI.WeakPinned.Grid.integral_shares_nat_periods line 286
  35. lemma OAI.WeakPinned.Grid.integral_fine_shares line 297

    Source documentation

    The fine-scale shift is the original unit shift. Its sharing law is still the correct uniform-modulo-side law, not a fresh independent grid.

    lemma integral_fine_shares (n : ℕ) (x y : ℝ) :
    (∫ ω, shares ((2:ℝ)^(- (n:ℤ))) (shift 0 ω) x y ∂axisLaw) =
      max 0 (1-|x-y|/((2:ℝ)^(- (n:ℤ)))) := by
…

    Mentions: OAI.WeakPinned.Grid.shares, OAI.WeakPinned.Grid.shift, OAI.WeakPinned.Grid.axisLaw

  36. lemma OAI.WeakPinned.Grid.binaryStep_ae line 313
  37. lemma OAI.WeakPinned.Grid.axis_increment_ae line 322
  38. lemma OAI.WeakPinned.Grid.bins_nested_ae line 329
  39. abbrev OAI.WeakPinned.Grid.GridSample line 341

    Source documentation

    Both independent axis constructions, before phase and rotation.

    abbrev GridSample := (ℕ → ℝ) × (ℕ → ℝ)
  40. def OAI.WeakPinned.Grid.squareLaw line 342
  41. instance OAI.WeakPinned.Grid.squareLaw_probability line 343
  42. def OAI.WeakPinned.Grid.shiftZ line 347
  43. def OAI.WeakPinned.Grid.shareAt line 349
  44. lemma OAI.WeakPinned.Grid.measurableSet_shareAt line 353
  45. lemma OAI.WeakPinned.Grid.integral_shiftZ_shares line 364
  46. lemma OAI.WeakPinned.Grid.sharing_probability line 376
  47. lemma OAI.WeakPinned.Grid.max_sharing_bound line 392
  48. lemma OAI.WeakPinned.Grid.separation_probability_le line 403
  49. lemma OAI.WeakPinned.Grid.share_eventually_exists line 411
  50. lemma OAI.WeakPinned.Grid.axis_nestedZ_ae line 424
  51. lemma OAI.WeakPinned.Grid.shareAt_nested_ae line 440
  52. lemma OAI.WeakPinned.Grid.shareAt_symm line 446
  53. lemma OAI.WeakPinned.Grid.shareAt_trans line 448
  54. lemma OAI.WeakPinned.Grid.shareAt_bddBelow line 452
  55. def OAI.WeakPinned.Grid.minScale line 465
  56. def OAI.WeakPinned.Grid.gridDepth line 467
  57. lemma OAI.WeakPinned.Grid.minScale_symm line 470
  58. lemma OAI.WeakPinned.Grid.minScale_mem line 477
  59. lemma OAI.WeakPinned.Grid.minScale_le line 481
  60. lemma OAI.WeakPinned.Grid.shareAt_iff_minScale_le line 485
  61. lemma OAI.WeakPinned.Grid.minScale_eq_iff line 495
  62. lemma OAI.WeakPinned.Grid.measurable_minScale line 525
  63. lemma OAI.WeakPinned.Grid.measurable_gridDepth line 553
  64. lemma OAI.WeakPinned.Grid.gridDepth_ultra_ae line 557
  65. lemma OAI.WeakPinned.Grid.error_upper_ae line 586

    Source documentation

    Euclidean norm can subsequently be used for R: only its elementary comparison with the two coordinate gaps is needed for the tail bound.

    lemma error_upper_ae {x y : ℝ × ℝ} (hxy : x ≠ y) {R : ℝ} (hR : 0 < R)
    (hgap : R ≤ |x.1-y.1|+|x.2-y.2|) :
    ∀ᵐ ω ∂squareLaw, gridDepth ω x y + Real.log R ≤ Real.log 2 := by
…

    Mentions: OAI.WeakPinned.Grid.squareLaw, OAI.WeakPinned.Grid.gridDepth

  66. lemma OAI.WeakPinned.Grid.error_lower_tail line 600
  67. lemma OAI.WeakPinned.Grid.error_abs_tail line 627
  68. lemma OAI.WeakPinned.Grid.error_abs_lintegral_le line 650
  69. lemma OAI.WeakPinned.Grid.error_integrable line 675
  70. lemma OAI.WeakPinned.Grid.mean_abs_error_le line 687
  71. lemma OAI.WeakPinned.Grid.minScale_cdf line 698
  72. lemma OAI.WeakPinned.Grid.minScale_law_same_gaps line 712
  73. lemma OAI.WeakPinned.Grid.mean_depth_same_gaps line 724
  74. lemma OAI.WeakPinned.Grid.minScale_law_double line 733
  75. lemma OAI.WeakPinned.Grid.gridDepth_integrable line 758
  76. lemma OAI.WeakPinned.Grid.mean_depth_double line 771
  77. lemma OAI.WeakPinned.Grid.measurableSet_shareAt_param line 797

    Source documentation

    Parameter measurability, needed before integrating orientation and phase.

    lemma measurableSet_shareAt_param {T : Type u1} [MeasurableSpace T]
    {W : T → GridSample} {X Y : T → ℝ × ℝ}
    (hW : Measurable W) (hX : Measurable X) (hY : Measurable Y) (m : ℤ) :
    MeasurableSet {t | shareAt m (W t) (X t) (Y t)} := by
…

    Mentions: OAI.WeakPinned.Grid.GridSample, OAI.WeakPinned.Grid.shareAt

  78. lemma OAI.WeakPinned.Grid.measurable_minScale_param line 810
  79. lemma OAI.WeakPinned.Grid.measurable_gridDepth_param line 832
  80. def OAI.WeakPinned.Grid.polarPair line 839
  81. def OAI.WeakPinned.Grid.polarMean line 841
  82. lemma OAI.WeakPinned.Grid.zero_ne_polarPair line 844
  83. lemma OAI.WeakPinned.Grid.polarPair_gaps line 853
  84. lemma OAI.WeakPinned.Grid.polarMean_integral line 869
  85. lemma OAI.WeakPinned.Grid.polarMean_bound line 874
  86. lemma OAI.WeakPinned.Grid.measurable_polarPair line 887
  87. lemma OAI.WeakPinned.Grid.measurable_polarMean line 891
  88. lemma OAI.WeakPinned.Grid.polarPair_double line 901
  89. lemma OAI.WeakPinned.Grid.polarMean_period_phase line 906
  90. lemma OAI.WeakPinned.Grid.polarMean_period_angle line 913
  91. lemma OAI.WeakPinned.Grid.uniformInterval_integral line 917
  92. lemma OAI.WeakPinned.Grid.uniformInterval_period_shift line 922
  93. lemma OAI.WeakPinned.Grid.uniformInterval_period_sub line 930
  94. def OAI.WeakPinned.Grid.kappa line 940

    Source documentation

    The universal archimedean error mean, before any configuration is chosen.

    def kappa : ℝ := ∫ ξ, ∫ θ, polarMean (-ξ) θ
…

    Mentions: OAI.WeakPinned.Grid.polarMean

  95. lemma OAI.WeakPinned.Grid.polar_average_constant line 943
  96. def OAI.WeakPinned.Grid.rotateC line 956
  97. def OAI.WeakPinned.Grid.rotatePair line 959
  98. lemma OAI.WeakPinned.Grid.rotateC_sub line 962
  99. lemma OAI.WeakPinned.Grid.norm_rotateC line 966
  100. lemma OAI.WeakPinned.Grid.rotatePair_ne line 971
  101. lemma OAI.WeakPinned.Grid.rotatePair_gaps line 981
  102. lemma OAI.WeakPinned.Grid.rotateC_polar line 994
  103. lemma OAI.WeakPinned.Grid.exp_polarPair line 1007
  104. lemma OAI.WeakPinned.Grid.rotated_mean line 1012
  105. abbrev OAI.WeakPinned.Grid.FullSample line 1024
  106. def OAI.WeakPinned.Grid.phaseLaw line 1026
  107. def OAI.WeakPinned.Grid.fullLaw line 1029
  108. instance OAI.WeakPinned.Grid.phaseLaw_probability line 1031
  109. instance OAI.WeakPinned.Grid.fullLaw_probability line 1036
  110. def OAI.WeakPinned.Grid.depth line 1040

    Source documentation

    Actual jointly defined hierarchy depth in the original complex plane.

    def depth (ω : FullSample) (z w : ℂ) : ℝ :=
…

    Mentions: OAI.WeakPinned.Grid.FullSample

  111. def OAI.WeakPinned.Grid.error line 1043
  112. lemma OAI.WeakPinned.Grid.measurable_rotatePair line 1045
  113. lemma OAI.WeakPinned.Grid.measurable_depth line 1049
  114. lemma OAI.WeakPinned.Grid.measurable_error line 1056
  115. lemma OAI.WeakPinned.Grid.error_fixed_phase line 1059
  116. lemma OAI.WeakPinned.Grid.error_integrable_fixed line 1066
  117. lemma OAI.WeakPinned.Grid.mean_abs_error_fixed line 1073
  118. lemma OAI.WeakPinned.Grid.error_integrable_full line 1080
  119. lemma OAI.WeakPinned.Grid.mean_error_fixed line 1090
  120. lemma OAI.WeakPinned.Grid.measurable_shifted_polarMean line 1102
  121. lemma OAI.WeakPinned.Grid.mean_error_full line 1111
  122. lemma OAI.WeakPinned.Grid.abs_error_tail_full line 1121
  123. lemma OAI.WeakPinned.Grid.mean_abs_error_full line 1144
  124. lemma OAI.WeakPinned.Grid.depth_symm line 1153
  125. lemma OAI.WeakPinned.Grid.depth_ultra_ae line 1157