OAI/Geometry/PlaneColoring/WeakColoring.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EuclideanFiveColor.PlaneL2 line 9
  2. def OAI.EuclideanFiveColor.shiftL2 line 10
  3. lemma OAI.EuclideanFiveColor.shiftL2_ae line 12
  4. lemma OAI.EuclideanFiveColor.shiftL2_continuous line 14
  5. lemma OAI.EuclideanFiveColor.correlation_continuous line 17
  6. lemma OAI.EuclideanFiveColor.product_zero_of_inner_zero line 19
  7. lemma OAI.EuclideanFiveColor.all_parameters_product_zero line 31

    Source documentation

    AE exclusions over any full-support parameter measure upgrade to every parameter.

    lemma all_parameters_product_zero {T : Type*} [TopologicalSpace T] [MeasurableSpace T]
    (μ : Measure T) [μ.IsOpenPosMeasure] (d : T → ℂ) (hd : Continuous d)
    (f : PlaneL2) (hf : ∀ᵐ x ∂volume, 0 ≤ f x)
    (ho : ∀ᵐ t ∂μ, ∀ᵐ x ∂(volume : Measure ℂ), f x*f (x+d t)=0) :
    ∀ t : T, ∀ᵐ x ∂(volume : Measure ℂ), f x*f (x+d t)=0 := by
…

    Mentions: OAI.EuclideanFiveColor.PlaneL2

  8. def OAI.EuclideanFiveColor.truncatedClass line 60
  9. lemma OAI.EuclideanFiveColor.truncatedClass_measurable line 62
  10. lemma OAI.EuclideanFiveColor.truncatedClass_finite line 65
  11. def OAI.EuclideanFiveColor.truncatedVector line 68
  12. lemma OAI.EuclideanFiveColor.truncatedVector_ae line 70
  13. lemma OAI.EuclideanFiveColor.weak_all_directions line 73
  14. def OAI.EuclideanFiveColor.DensityOne line 119
  15. lemma OAI.EuclideanFiveColor.densityOne_disjoint line 122
  16. lemma OAI.EuclideanFiveColor.densityOne_translate line 134
  17. lemma OAI.EuclideanFiveColor.direction_exists line 145
  18. lemma OAI.EuclideanFiveColor.weak_density_proper line 149
  19. lemma OAI.EuclideanFiveColor.ae_density_actual line 164