OAI/MeasureTheory/CompactFactors/Factors.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.EuclideanFiveColor.OrbitSpace line 41
  2. def OAI.EuclideanFiveColor.OrbitSpace.equiv line 46
  3. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 52) line 52
  4. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 53) line 53
  5. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 54) line 54
  6. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 55) line 55
  7. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 56) line 56
  8. lemma OAI.EuclideanFiveColor.OrbitSpace.ext line 58
  9. lemma OAI.EuclideanFiveColor.OrbitSpace.continuous_val line 61
  10. lemma OAI.EuclideanFiveColor.OrbitSpace.continuous_mk line 63
  11. lemma OAI.EuclideanFiveColor.OrbitSpace.measurable_val line 65
  12. lemma OAI.EuclideanFiveColor.OrbitSpace.measurable_mk line 66
  13. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 68) line 68
  14. lemma OAI.EuclideanFiveColor.OrbitSpace.smul_val line 73
  15. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 76) line 76
  16. instance OAI.EuclideanFiveColor.OrbitSpace.(instance at line 79) line 79
  17. def OAI.EuclideanFiveColor.OrbitFactor.orbit line 88
  18. lemma OAI.EuclideanFiveColor.OrbitFactor.measurable_orbit line 91
  19. lemma OAI.EuclideanFiveColor.OrbitFactor.orbit_equivariant line 96
  20. def OAI.EuclideanFiveColor.OrbitFactor.extend line 101
  21. lemma OAI.EuclideanFiveColor.OrbitFactor.measurable_extend line 104
  22. lemma OAI.EuclideanFiveColor.OrbitFactor.extend_equivariant line 109
  23. lemma OAI.EuclideanFiveColor.OrbitFactor.orbit_one line 116
  24. lemma OAI.EuclideanFiveColor.OrbitFactor.measurable_extend_compactSigma line 130
  25. lemma OAI.EuclideanFiveColor.OrbitFactor.compact_orbit_extension line 146

    Source documentation

    The orbit factor generated by a compact scalar function is an actual compact extension; the finite module is projected onto that factor.

    lemma compact_orbit_extension (μ : Measure X) [IsProbabilityMeasure μ]
    (q : X → Y) (hq : Measurable q)
    (hpres : ∀ k : K, MeasurePreserving (fun x : X => k • x) μ μ)
    (hqcov : ∀ k : K, ∀ᵐ x ∂μ, q (k • x) = k • q x)
    (H : X → ℂ) (hH : Measurable H) (hc : Compact (K := K) μ q H)
…
  26. lemma OAI.EuclideanFiveColor.KernelCompact.compact_applyKernel line 173
  27. theorem OAI.EuclideanFiveColor.CompactTower.strict_compact_successor line 206

    Source documentation

    The strict compact-successor step of the compact tower. The new coordinate is constructed from a centered invariant conditional-product kernel.

    theorem strict_compact_successor (μ : Measure X) [IsProbabilityMeasure μ]
    [ErgodicSMul K X μ] (q : X → Y) (hq : Measurable q)
    (hqcov : ∀ k : K, ∀ᵐ x ∂μ, q (k • x) = k • q x)
    (hn : ¬ ErgodicSMul K (X × X) (RelativeProduct.law μ q hq)) :
    ∃ H : X → ℂ, Measurable H ∧ (∀ x, ‖H x‖ ≤ 2) ∧
      (¬ ∃ b : Y → ℂ, Measurable b ∧ H =ᵐ[μ] b ∘ q) ∧
      (∀ F : Y × OrbitSpace K → ℂ, Measurable F →
        (∃ C : ℝ, ∀ z, ‖F z‖ ≤ C) →
        Compact (K := K) (μ.map (extend (K := K) q H)) Prod.fst F) := by
…

    Mentions: OAI.EuclideanFiveColor.RelativeProduct.law, OAI.EuclideanFiveColor.OrbitSpace

  28. def OAI.EuclideanFiveColor.FactorCode.scalar line 243
  29. lemma OAI.EuclideanFiveColor.FactorCode.scalar_measurable line 246
  30. lemma OAI.EuclideanFiveColor.FactorCode.scalar_injective line 249
  31. lemma OAI.EuclideanFiveColor.FactorCode.scalar_embedding line 255
  32. lemma OAI.EuclideanFiveColor.FactorCode.scalar_bound line 258
  33. def OAI.EuclideanFiveColor.FactorCode.encode line 267
  34. lemma OAI.EuclideanFiveColor.FactorCode.encode_measurable line 269
  35. lemma OAI.EuclideanFiveColor.FactorCode.encode_equivariant line 273
  36. lemma OAI.EuclideanFiveColor.FactorCode.encode_bound line 277
  37. def OAI.EuclideanFiveColor.FactorCode.decode line 280
  38. lemma OAI.EuclideanFiveColor.FactorCode.decode_measurable line 282
  39. lemma OAI.EuclideanFiveColor.FactorCode.decode_encode line 286
  40. lemma OAI.EuclideanFiveColor.FactorCode.encode_as_comp line 292
  41. def OAI.EuclideanFiveColor.FactorLp.space line 305
  42. lemma OAI.EuclideanFiveColor.FactorLp.isClosed line 309
  43. lemma OAI.EuclideanFiveColor.FactorLp.exists_rep line 314
  44. lemma OAI.EuclideanFiveColor.FactorLp.mem_of_rep line 321
  45. lemma OAI.EuclideanFiveColor.FactorLp.le_of_factor line 326
  46. lemma OAI.EuclideanFiveColor.FactorLp.factor_of_le line 334
  47. def OAI.EuclideanFiveColor.CountableApprox.truncate line 356
  48. lemma OAI.EuclideanFiveColor.CountableApprox.truncate_measurable line 358
  49. lemma OAI.EuclideanFiveColor.CountableApprox.truncate_mono line 361
  50. lemma OAI.EuclideanFiveColor.CountableApprox.truncate_generate line 371
  51. lemma OAI.EuclideanFiveColor.CountableApprox.bounded_approximation line 385
  52. def OAI.EuclideanFiveColor.ChainJoin.joint line 401
  53. def OAI.EuclideanFiveColor.ChainJoin.code line 403
  54. lemma OAI.EuclideanFiveColor.ChainJoin.joint_measurable line 406
  55. lemma OAI.EuclideanFiveColor.ChainJoin.code_measurable line 410
  56. lemma OAI.EuclideanFiveColor.ChainJoin.code_equivariant line 414
  57. lemma OAI.EuclideanFiveColor.ChainJoin.le_code line 418
  58. lemma OAI.EuclideanFiveColor.ChainJoin.joint_equivariant line 429
  59. lemma OAI.EuclideanFiveColor.ChainJoin.finite_upper line 436
  60. lemma OAI.EuclideanFiveColor.ChainJoin.approximation line 455
  61. lemma OAI.EuclideanFiveColor.SeparableZorn.countable_cover line 500
  62. lemma OAI.EuclideanFiveColor.SeparableZorn.exists_maximal line 523
  63. structure OAI.EuclideanFiveColor.CodedMax.Model line 551
  64. instance OAI.EuclideanFiveColor.CodedMax.(instance at line 557) line 557
  65. lemma OAI.EuclideanFiveColor.CodedMax.exists_maximal line 562