OAI/MeasureTheory/CompactFactors/RelativeCenters.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EuclideanFiveColor.UniformFibers.finite_uniform_fibers line 40
2. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.finite_uniform_centers line 89

   Source documentation

   The conditional center law has finitely many, equally weighted atoms. The original cosets need not form a standard Borel quotient.

   theorem finite_uniform_centers (μ : ProbabilityMeasure G) {a : ℝ≥0∞}
       (ha : 0 < a) (hs : ∀ᵐ z ∂(μ : Measure G), (μ : Measure G) (e.coset z) = a) :
       ∃ S : Finset G, S.Nonempty ∧
         (∀ b ∈ S, (μ : Measure G) ((e.center μ) ⁻¹' {b}) = a) ∧
         (∀ᵐ z ∂(μ : Measure G), e.center μ z ∈ S) ∧
         (S.card : ℝ≥0∞) * a = 1 := by
   …

3. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.center_law_ordinary line 102

   Source documentation

   Wildness survives the measurable recentering construction.

   theorem center_law_ordinary (μ : ProbabilityMeasure G) :
       (μ.map (e.center μ) : Measure G) e.ordinary =
         (μ : Measure G) e.ordinary := by
   …

4. theorem OAI.EuclideanFiveColor.ErgodicSupport.ae_eq_const_of_invariant line 121

   Source documentation

   The invariant-function consequence of group-action ergodicity, with an individual almost-everywhere identity for each group element.

   theorem ae_eq_const_of_invariant {f : X → V} (hf : Measurable f)
       (hi : ∀ k : K, ∀ᵐ x ∂μ, f (k • x) = f x) :
       ∃ v : V, f =ᵐ[μ] (fun _ => v) := by
   …

5. lemma OAI.EuclideanFiveColor.KernelSupport.compProd_map_base line 140
6. lemma OAI.EuclideanFiveColor.KernelSupport.condDistrib_comp_equiv line 154
7. lemma OAI.EuclideanFiveColor.KernelSupport.condDistrib_equivariant line 169

   Source documentation

   Changing both coordinates of a conditional law by invertible measurable maps commutes with conditional sampling.

   lemma condDistrib_equivariant [StandardBorelSpace Z] [Nonempty Z]
       (μ : Measure X) [IsFiniteMeasure μ]
       (f : X → Z) (p : X → Y) (hf : Measurable f) (hp : Measurable p)
       (S : X ≃ᵐ X) (R : Y ≃ᵐ Y) (T : Z → Z) (hT : Measurable T)
       (hS : MeasurePreserving S μ μ)
       (hRp : p ∘ S =ᵐ[μ] R ∘ p) (hTf : f ∘ S =ᵐ[μ] T ∘ f) :
       ∀ᵐ y ∂μ.map p, condDistrib f p μ (R y) = (condDistrib f p μ y).map T := by
   …

8. def OAI.EuclideanFiveColor.RelativeCenters.probabilityKernel line 218
9. lemma OAI.EuclideanFiveColor.RelativeCenters.measurable_probabilityKernel line 222
10. def OAI.EuclideanFiveColor.RelativeCenters.cosetMass line 225
11. lemma OAI.EuclideanFiveColor.RelativeCenters.measurable_cosetMass line 228
12. def OAI.EuclideanFiveColor.RelativeCenters.differenceLaw line 235

    Source documentation

    The relative difference law uses two independent samples of the same conditional probability law; it is not an independent marginal difference.

    noncomputable def differenceLaw (ν : Measure Y) (κ : Kernel Y G) [IsMarkovKernel κ] :
        Measure G := ((κ ×ₖ κ) ∘ₘ ν).map (fun p : G × G => p.1 / p.2)

13. lemma OAI.EuclideanFiveColor.RelativeCenters.differenceLaw_ordinary line 238
14. lemma OAI.EuclideanFiveColor.RelativeCenters.sampledMass_integral line 256
15. theorem OAI.EuclideanFiveColor.RelativeCenters.positive_mass_finite_centers line 267

    Source documentation

    Positive relative mass and ergodicity force a fixed positive mass for almost all sampled cosets. The finite-center conclusion follows without a quotient measurable space for the ordinary-character subgroup.

    theorem positive_mass_finite_centers [StandardBorelSpace G]
        [MeasurableSingletonClass G]
        {K : Type*} [SMul K X]
        (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul K X μ]
        (d : X → G) (p : X → Y) (hd : Measurable d) (hp : Measurable p)
        (hi : ∀ k : K, ∀ᵐ x ∂μ,
          cosetMass e (condDistrib d p μ) (p (k • x), d (k • x)) =
            cosetMass e (condDistrib d p μ) (p x, d x))
        (hpos : 0 < differenceLaw (μ.map p) (condDistrib d p μ) e.ordinary) :
        ∃ a : ℝ≥0∞, 0 < a ∧
          (∀ᵐ x ∂μ, cosetMass e (condDistrib d p μ) (p x, d x) = a) ∧
          ∀ᵐ y ∂μ.map p, ∃ S : Finset G, S.Nonempty ∧
    …

    Mentions: OAI.EuclideanFiveColor.RelativeCenters.cosetMass, OAI.EuclideanFiveColor.RelativeCenters.differenceLaw

16. lemma OAI.EuclideanFiveColor.RelativeCenters.sampledMass_invariant line 306
17. def OAI.EuclideanFiveColor.RelativeCenters.centerMap line 333
18. lemma OAI.EuclideanFiveColor.RelativeCenters.measurable_centerMap line 337
19. lemma OAI.EuclideanFiveColor.RelativeCenters.centerMap_mem_ordinary_iff line 344
20. lemma OAI.EuclideanFiveColor.RelativeCenters.centerMap_law_ordinary line 349
21. lemma OAI.EuclideanFiveColor.RelativeCenters.centerMap_equivariant line 365
22. lemma OAI.EuclideanFiveColor.RelativeCenters.dependentMapKernel_apply line 396
23. lemma OAI.EuclideanFiveColor.RelativeCenters.compProd_dependentMap line 404
24. def OAI.EuclideanFiveColor.RelativeCenters.centerKernel line 419
25. lemma OAI.EuclideanFiveColor.RelativeCenters.measurable_fiberCenter line 422
26. instance OAI.EuclideanFiveColor.RelativeCenters.centerKernel_markov line 427
27. lemma OAI.EuclideanFiveColor.RelativeCenters.centerKernel_apply line 431
28. lemma OAI.EuclideanFiveColor.RelativeCenters.condDistrib_centerMap line 435
29. lemma OAI.EuclideanFiveColor.RelativeCenters.centerKernel_comp_map line 449
30. theorem OAI.EuclideanFiveColor.RelativeCenters.finite_center_reduction line 461
31. instance OAI.PlaneFiveColor.Spectral.dualStandardBorelSpace line 520
32. instance OAI.PlaneFiveColor.Spectral.dualMulDistribAction line 525
33. instance OAI.PlaneFiveColor.Spectral.dualMeasurableConstSMul line 529
34. def OAI.PlaneFiveColor.Spectral.ordinaryEmbedding line 532
35. theorem OAI.PlaneFiveColor.Spectral.ordinaryEmbedding_j line 535
36. theorem OAI.PlaneFiveColor.Spectral.ordinaryEmbedding_ordinary line 536
37. def OAI.PlaneFiveColor.Spectral.frequencyIsometry line 538
38. def OAI.PlaneFiveColor.Spectral.frequencyRotation line 546
39. theorem OAI.PlaneFiveColor.Spectral.frequencyRotation_apply line 549
40. theorem OAI.PlaneFiveColor.Spectral.action_ordinaryEmbedding line 552
41. theorem OAI.PlaneFiveColor.Spectral.wild_map_of_equivariant line 560
42. theorem OAI.PlaneFiveColor.Spectral.exact_finite_center_reduction line 573