OAI/Analysis/PlaneSpectrum/Ergodicity.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlaneFiveColor.Spectral.normF line 12
  2. lemma OAI.PlaneFiveColor.Spectral.normF_coe line 18
  3. lemma OAI.PlaneFiveColor.Spectral.normF_pos line 19
  4. lemma OAI.PlaneFiveColor.Spectral.projectedMass_vanish line 30
  5. lemma OAI.PlaneFiveColor.Spectral.fourier_vanish_of_terminal line 37
  6. lemma OAI.PlaneFiveColor.Spectral.ergodic_wild_fourier line 52
  7. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_mem_closedConvexHull line 69
  8. structure OAI.EuclideanFiveColor.ConvexAverage line 90
  9. def OAI.EuclideanFiveColor.ConvexAverage.apply line 99
  10. lemma OAI.EuclideanFiveColor.ConvexAverage.norm_le line 100
  11. lemma OAI.EuclideanFiveColor.ConvexAverage.of_mem_convexHull line 107
  12. lemma OAI.EuclideanFiveColor.Amenable.Mean.exists_finite_approx line 122
  13. def OAI.EuclideanFiveColor.ConvexAverage.bm line 141
  14. lemma OAI.EuclideanFiveColor.ConvexAverage.bm_apply line 142
  15. lemma OAI.EuclideanFiveColor.ConvexAverage.bm_bound line 144
  16. lemma OAI.EuclideanFiveColor.ConvexAverage.l2_bm line 147
  17. def OAI.EuclideanFiveColor.InvariantSequence.limit line 157
  18. lemma OAI.EuclideanFiveColor.InvariantSequence.limit_measurable line 158
  19. lemma OAI.EuclideanFiveColor.InvariantSequence.limit_fixed line 159
  20. lemma OAI.EuclideanFiveColor.InvariantSequence.exists_averages line 163
  21. lemma OAI.EuclideanFiveColor.ConvexAverage.setIntegral_bm line 187
  22. lemma OAI.EuclideanFiveColor.ConvexAverage.setIntegral_of_limit line 201
  23. def OAI.EuclideanFiveColor.ErgodicCriterion.testSet line 215
  24. lemma OAI.EuclideanFiveColor.ErgodicCriterion.measurable_testSet line 216
  25. lemma OAI.EuclideanFiveColor.ErgodicCriterion.testSet_union line 218
  26. lemma OAI.EuclideanFiveColor.ErgodicCriterion.pi_testSet line 220
  27. lemma OAI.EuclideanFiveColor.ErgodicCriterion.generate_testSet line 223
  28. def OAI.EuclideanFiveColor.ErgodicCriterion.test line 231
  29. lemma OAI.EuclideanFiveColor.ErgodicCriterion.test_apply line 234
  30. lemma OAI.EuclideanFiveColor.ErgodicCriterion.ergodic_of_test_limits line 238
  31. def OAI.EuclideanFiveColor.InvariantDecomposition.code line 289
  32. lemma OAI.EuclideanFiveColor.InvariantDecomposition.code_measurable line 291
  33. lemma OAI.EuclideanFiveColor.InvariantDecomposition.code_fixed line 294
  34. lemma OAI.EuclideanFiveColor.InvariantDecomposition.fiber_invariant line 297
  35. lemma OAI.EuclideanFiveColor.InvariantDecomposition.fiber_ergodic line 309
  36. instance OAI.PlaneFiveColor.Spectral.(instance at line 327) line 327
  37. lemma OAI.PlaneFiveColor.Spectral.smul_ergodic_of_rot line 328
  38. lemma OAI.PlaneFiveColor.Spectral.wild_fourier line 335

    Source documentation

    The arbitrary invariant wild case, obtained from actual conditional ergodic fibers.

    lemma wild_fourier (μ : Measure D) [IsProbabilityMeasure μ]
    (hw : IsWild μ) (z : E) (hz : z ≠ 0) : ∫ d, (eval z d : ℂ) ∂μ = 0 := by
…

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.eval

  39. lemma OAI.PlaneFiveColor.Spectral.finite_wild_fourier line 364
  40. lemma OAI.PlaneFiveColor.Spectral.vectorMeasure_invariant line 383
  41. lemma OAI.PlaneFiveColor.Spectral.residual_fourier line 403