OAI/Analysis/PlaneSpectrum/Energy.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.MovingMean.approxAt line 16
  2. lemma OAI.EuclideanFiveColor.MovingMean.approx_norm_le line 17
  3. lemma OAI.EuclideanFiveColor.MovingMean.approx_has_limit line 20
  4. def OAI.EuclideanFiveColor.MovingMean.meanAt line 33

    Source documentation

    The invariant meanAt b, as the limit of the multiplicity-preserving averages.

    def meanAt (f : G →ᵇ ℝ) : ℝ :=
…
  5. lemma OAI.EuclideanFiveColor.MovingMean.tendsto_approx line 36
  6. lemma OAI.EuclideanFiveColor.MovingMean.mean_add line 40
  7. lemma OAI.EuclideanFiveColor.MovingMean.mean_smul line 45
  8. lemma OAI.EuclideanFiveColor.MovingMean.mean_const line 50
  9. lemma OAI.EuclideanFiveColor.MovingMean.mean_nonneg line 56
  10. lemma OAI.EuclideanFiveColor.MovingMean.mean_norm_le line 60
  11. lemma OAI.EuclideanFiveColor.MovingMean.mean_shift line 64
  12. def OAI.EuclideanFiveColor.MovingMean.meanCLM line 75

    Source documentation

    A normalized positive shift-invariant continuous real linear functional.

    def meanCLM : (G →ᵇ ℝ) →L[ℝ] ℝ :=
…
  13. lemma OAI.EuclideanFiveColor.MovingMean.meanCLM_apply line 80
  14. def OAI.EuclideanFiveColor.MovingMean.toMean line 82
  15. def OAI.EuclideanFiveColor.MovingMean.cubeSupport line 92
  16. lemma OAI.EuclideanFiveColor.MovingMean.cube_le_of_support line 95
  17. lemma OAI.EuclideanFiveColor.MovingMean.syndetic_of_all_means line 117

    Source documentation

    If every invariant mean gives a bounded function a value above c, its strict c-superlevel set has finitely many translates covering the group.

    lemma syndetic_of_all_means (f : G →ᵇ ℝ) (c : ℝ)
    (hf : ∀ M : Amenable.Mean G, c < M.map f) :
    ∃ S : Finset G, ∀ v : G, ∃ s ∈ S, c < f (v+s) := by
…

    Mentions: OAI.EuclideanFiveColor.Amenable.Mean

  18. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.energy line 142
  19. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.energy_apply line 144
  20. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.energy_mean_eq_of_meanNorm_zero line 146
  21. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.avg_const line 171
  22. def OAI.EuclideanFiveColor.BoundedMeasurable.normSquare line 181
  23. lemma OAI.EuclideanFiveColor.BoundedMeasurable.normSquare_apply line 182
  24. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integral_normSquare line 185
  25. lemma OAI.EuclideanFiveColor.BoundedMeasurable.inner_normSquare line 187
  26. lemma OAI.EuclideanFiveColor.BoundedMeasurable.avg_orbit_const line 197
  27. lemma OAI.EuclideanFiveColor.BoundedMeasurable.pair_energy_mean line 217
  28. lemma OAI.EuclideanFiveColor.BoundedMeasurable.energy_two_orbits line 243
  29. lemma OAI.EuclideanFiveColor.BoundedMeasurable.two_orbit_energy_mean line 258
  30. lemma OAI.EuclideanFiveColor.BoundedMeasurable.factor_ergodic line 276
  31. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_pair_energy line 312
  32. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_integer_pair_energy line 323
  33. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_integer_triple_energy line 342
  34. def OAI.PlaneFiveColor.Spectral.char line 368

    Source documentation

    The exact evaluation character, as a bounded measurable function.

    def char (z : E) : Func D := ⟨fun d => (eval z d : ℂ), measurable_eval_coe z,
…

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

  35. lemma OAI.PlaneFiveColor.Spectral.char_apply line 370
  36. lemma OAI.PlaneFiveColor.Spectral.norm_char line 371
  37. lemma OAI.PlaneFiveColor.Spectral.char_zero line 372
  38. lemma OAI.PlaneFiveColor.Spectral.char_add line 373
  39. lemma OAI.PlaneFiveColor.Spectral.char_neg line 376
  40. lemma OAI.PlaneFiveColor.Spectral.char_act line 380
  41. def OAI.PlaneFiveColor.Spectral.projectedMass line 384
  42. lemma OAI.PlaneFiveColor.Spectral.projectedMass_nonneg line 385
  43. lemma OAI.PlaneFiveColor.Spectral.projected_char_bound line 386
  44. lemma OAI.PlaneFiveColor.Spectral.projectedMass_le_one line 390
  45. lemma OAI.PlaneFiveColor.Spectral.projectedMass_zero line 397
  46. lemma OAI.PlaneFiveColor.Spectral.differenceFourier_projectedMass line 408
  47. lemma OAI.PlaneFiveColor.Spectral.projectedMass_rotation line 420
  48. lemma OAI.PlaneFiveColor.Spectral.projectedMass_radial line 432