OAI/Geometry/PlaneColoring/Compactness.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.weakHilbert line 11
  2. lemma OAI.EuclideanFiveColor.weakHilbert_apply line 13
  3. lemma OAI.EuclideanFiveColor.exists_finite_weak_subseq line 14
  4. abbrev OAI.EuclideanFiveColor.RealL2 line 43
  5. def OAI.EuclideanFiveColor.oneL2 line 44
  6. lemma OAI.EuclideanFiveColor.oneL2_ae line 45
  7. lemma OAI.EuclideanFiveColor.weak_limit_nonneg line 48
  8. lemma OAI.EuclideanFiveColor.weak_limit_le_one line 58
  9. lemma OAI.EuclideanFiveColor.weak_limit_sum line 67
  10. def OAI.EuclideanFiveColor.Typical line 83
  11. def OAI.EuclideanFiveColor.TypicalSampling line 84
  12. lemma OAI.EuclideanFiveColor.ae_typicalSampling line 86
  13. def OAI.EuclideanFiveColor.sampleFn line 97
  14. lemma OAI.EuclideanFiveColor.sampleFn_measurable line 99
  15. lemma OAI.EuclideanFiveColor.sampleFn_nonneg line 103
  16. lemma OAI.EuclideanFiveColor.sampleFn_le_one line 105
  17. lemma OAI.EuclideanFiveColor.sampleFn_memLp line 107
  18. def OAI.EuclideanFiveColor.sample line 111
  19. lemma OAI.EuclideanFiveColor.sample_ae line 113
  20. lemma OAI.EuclideanFiveColor.sample_norm_le line 115
  21. lemma OAI.EuclideanFiveColor.sample_sum line 122
  22. lemma OAI.EuclideanFiveColor.sampling_weak_compact line 130
  23. abbrev OAI.EuclideanFiveColor.WeakBall.Space line 159
  24. instance OAI.EuclideanFiveColor.WeakBall.(instance at line 160) line 160
  25. instance OAI.EuclideanFiveColor.WeakBall.(instance at line 161) line 161
  26. def OAI.EuclideanFiveColor.WeakBall.value line 163
  27. lemma OAI.EuclideanFiveColor.WeakBall.value_norm line 165
  28. lemma OAI.EuclideanFiveColor.WeakBall.value_eval line 168
  29. def OAI.EuclideanFiveColor.WeakBall.ofNorm line 170
  30. lemma OAI.EuclideanFiveColor.WeakBall.value_ofNorm line 174
  31. lemma OAI.EuclideanFiveColor.WeakBall.continuous_eval line 177
  32. lemma OAI.EuclideanFiveColor.WeakBall.tendsto_iff line 181
  33. lemma OAI.EuclideanFiveColor.bounded_test_error line 194
  34. lemma OAI.EuclideanFiveColor.weak_L2_to_weakStar line 209
  35. instance OAI.EuclideanFiveColor.(instance at line 250) line 250
  36. abbrev OAI.EuclideanFiveColor.TraceVector line 251
  37. def OAI.EuclideanFiveColor.traceValue line 252
  38. def OAI.EuclideanFiveColor.sampleCode line 255
  39. lemma OAI.EuclideanFiveColor.traceValue_sampleCode line 257
  40. def OAI.EuclideanFiveColor.sampleSet line 259
  41. def OAI.EuclideanFiveColor.IsTrace line 261
  42. lemma OAI.EuclideanFiveColor.trace_realization line 262
  43. lemma OAI.EuclideanFiveColor.trace_of_realization line 271
  44. lemma OAI.EuclideanFiveColor.exists_trace line 277
  45. lemma OAI.EuclideanFiveColor.isClosed_traceGraph line 284
  46. lemma OAI.EuclideanFiveColor.isCompact_traces line 286
  47. lemma OAI.EuclideanFiveColor.trace_limit line 289
  48. lemma OAI.EuclideanFiveColor.traceCode_tendsto_iff line 293
  49. lemma OAI.EuclideanFiveColor.trace_bounds line 297
  50. lemma OAI.EuclideanFiveColor.trace_realization_weakStar line 316
  51. lemma OAI.EuclideanFiveColor.exists_countable_essential_union line 345

    Source documentation

    A finite-measure essential union is generated by countably many members of the original family.

    lemma exists_countable_essential_union (A : I → Set X) (hm : ∀ i, MeasurableSet (A i)) :
    ∃ J : Set I, J.Countable ∧ ∀ i, A i ≤ᵐ[μ] (⋃ j ∈ J, A j) := by
…