OAI/Geometry/PlaneColoring/CircleTransport.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.tendsto_integral_of_local_cover line 11

    Source documentation

    A uniformly bounded nonnegative sequence converging locally in L¹ on a conull open cover converges globally in L¹ for a finite inner-regular measure.

    lemma tendsto_integral_of_local_cover {X I : Type*} [TopologicalSpace X] [T2Space X]
    [MeasurableSpace X] [OpensMeasurableSpace X] {μ : Measure X} [IsFiniteMeasure μ]
    [Measure.InnerRegularCompactLTTop μ] {F : ℕ → X → ℝ}
    (hF : ∀ n, Integrable (F n) μ) (hb : ∀ n x, 0 ≤ F n x ∧ F n x ≤ 1)
    (V : I → Set X) (hVo : ∀ i, IsOpen (V i)) (hfull : ∀ᵐ x ∂μ, x ∈ ⋃ i, V i)
    (hlocal : ∀ i, Tendsto (fun n => ∫ x in V i, F n x ∂μ) atTop (𝓝 0)) :
    Tendsto (fun n => ∫ x, F n x ∂μ) atTop (𝓝 0) := by
…
  2. lemma OAI.EuclideanFiveColor.bounded_difference_integrable line 71
  3. lemma OAI.EuclideanFiveColor.circleSum_tendsto_L1 line 80
  4. def OAI.EuclideanFiveColor.angularSum line 132
  5. lemma OAI.EuclideanFiveColor.angularSum_measurable line 134
  6. lemma OAI.EuclideanFiveColor.angularSum_chart line 137
  7. lemma OAI.EuclideanFiveColor.angularSum_quasiMeasurePreserving line 142
  8. lemma OAI.EuclideanFiveColor.angularSum_tendsto_L1 line 162
  9. def OAI.EuclideanFiveColor.samplingParameter line 184
  10. lemma OAI.EuclideanFiveColor.samplingParameter_tendsto line 185
  11. lemma OAI.EuclideanFiveColor.circleTarget_sampling line 189
  12. lemma OAI.EuclideanFiveColor.circleInverse_sampling line 196
  13. def OAI.EuclideanFiveColor.binaryPhi line 209
  14. def OAI.EuclideanFiveColor.binaryBeta line 210
  15. def OAI.EuclideanFiveColor.binaryTarget line 211
  16. def OAI.EuclideanFiveColor.binaryOther line 212
  17. lemma OAI.EuclideanFiveColor.binaryTarget_eq line 213
  18. lemma OAI.EuclideanFiveColor.binaryOther_eq line 217
  19. lemma OAI.EuclideanFiveColor.binaryPhi_trig line 220
  20. lemma OAI.EuclideanFiveColor.binaryBeta_trig line 244
  21. lemma OAI.EuclideanFiveColor.binary_geometry line 256
  22. lemma OAI.EuclideanFiveColor.binaryTarget_hasDeriv line 267
  23. lemma OAI.EuclideanFiveColor.binaryOther_hasDeriv line 271
  24. lemma OAI.EuclideanFiveColor.binary_nonparallel line 280
  25. lemma OAI.EuclideanFiveColor.binary_geometry_rotated line 296
  26. lemma OAI.EuclideanFiveColor.deriv_lower_surjective line 315
  27. def OAI.EuclideanFiveColor.derivLowerOrderIso line 329