OAI/MeasureTheory/CompactFactors/Approximation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The scalar finite bounded-module approximation in (source-4), and its finite-vector consequence. All functions are measurable bounded representatives.

  1. theorem OAI.EuclideanFiveColor.UniformEnumeration.list_of_uniform_atoms line 44
  2. theorem OAI.EuclideanFiveColor.UniformEnumeration.constant_uniform_lists line 69
  3. def OAI.EuclideanFiveColor.DifferenceInvariant.differenceLaw line 112
  4. lemma OAI.EuclideanFiveColor.DifferenceInvariant.invariant line 115
  5. def OAI.EuclideanFiveColor.CompactApproximation.Scalar line 156
  6. def OAI.EuclideanFiveColor.CompactApproximation.Vector line 164
  7. lemma OAI.EuclideanFiveColor.CompactApproximation.pi_dist_sq_le_sum line 173
  8. lemma OAI.EuclideanFiveColor.CompactApproximation.vector_of_scalar line 185
  9. lemma OAI.EuclideanFiveColor.KernelSupport.factor_smul_preserving line 284
  10. lemma OAI.PlaneFiveColor.Spectral.relative_difference_invariant line 305
  11. lemma OAI.PlaneFiveColor.Spectral.finite_encoding_approximation_of_compact line 320
  12. theorem OAI.PlaneFiveColor.Spectral.relative_singularity_successor line 384

    Source documentation

    The complete source successor implication. The predecessor assertion is universal in the equivariant wild map, as required by the transfinite induction.

    theorem relative_singularity_successor
    [StandardBorelSpace X] [Nonempty X] [StandardBorelSpace Y] [Nonempty Y]
    [StandardBorelSpace W] [Nonempty W]
    [MulAction K W] [MeasurableConstSMul K W]
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul K X μ]
    (d : X → D) (p : X → Y) (q : Y → W)
    (hd : Measurable d) (hp : Measurable p) (hq : Measurable q)
    (hde : ∀ k : K, ∀ᵐ x ∂μ, d (k • x) = k • d x)
    (hpe : ∀ k : K, ∀ᵐ x ∂μ, p (k • x) = k • p x)
    (hqe : ∀ k : K, ∀ᵐ y ∂μ.map p, q (k • y) = k • q y)
    (hwild : IsWild (μ.map d))
    (hc : CompactApproximation.Scalar (K := K) (μ.map p) q)
…

    Mentions: OAI.PlaneFiveColor.Spectral.K, OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild

  13. def OAI.EuclideanFiveColor.CompactApproximation.At line 425
  14. lemma OAI.EuclideanFiveColor.CompactApproximation.lift_at line 432