OAI/MeasureTheory/CompactFactors/Functions.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Bounded integral kernels yield finite-module orbit approximation. This implements the compact-tower construction without spectral projections: approximate the invariant kernel by finite rectangles first.

  1. def OAI.EuclideanFiveColor.CompactFunctions.At line 45
  2. def OAI.EuclideanFiveColor.CompactFunctions.Compact line 52
  3. lemma OAI.EuclideanFiveColor.CompactFunctions.at_of_finite line 55
  4. lemma OAI.EuclideanFiveColor.CompactFunctions.module_bound line 79
  5. lemma OAI.EuclideanFiveColor.CompactFunctions.dist_sq_add line 90
  6. lemma OAI.EuclideanFiveColor.CompactFunctions.dist_sq_chain line 96
  7. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_const line 102
  8. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_conj line 112
  9. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_add line 133
  10. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_mul line 188
  11. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_of_l2_approximation line 288
  12. lemma OAI.EuclideanFiveColor.Quantize.finite_measurable_choice line 332
  13. lemma OAI.EuclideanFiveColor.Quantize.compact_quantization line 369

    Source documentation

    A common finite net allows measurable nearest-bin selection for every measurable map into the compact set.

    lemma compact_quantization {s : Set A} (hs : IsCompact s) {ρ : ℝ} (hρ : 0 < ρ) :
    ∃ (n : ℕ) (c : Fin n → A), (∀ i, c i ∈ s) ∧
      ∀ a : Y → A, Measurable a → (∀ y, a y ∈ s) →
        ∃ f : Y → Fin n, Measurable f ∧ ∀ y, dist (a y) (c (f y)) < ρ := by
…
  14. lemma OAI.EuclideanFiveColor.CompactFunctions.combination_dist line 398
  15. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_lipschitz line 410

    Source documentation

    Functional calculus for an individual compact function. Quantizing the bounded coefficient arrays proves this directly, without a spectral theorem.

    lemma compact_lipschitz {μ : Measure X} [IsProbabilityMeasure μ] {q : X → Y} {H : X → ℂ}
    [MeasurableConstSMul K X] (hq : Measurable q) (hHm : Measurable H)
    (hH : Compact (K := K) μ q H) (f : ℂ → ℂ) (L : NNReal) (hLip : LipschitzWith L f) :
…

    Mentions: OAI.EuclideanFiveColor.CompactFunctions.Compact

  16. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_of_bounded_pointwise_limit line 514
  17. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_closed_preimage line 541
  18. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_neg line 584
  19. lemma OAI.EuclideanFiveColor.CompactFunctions.indicator_one_bound line 592
  20. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_compl line 595
  21. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_union line 606
  22. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_iUnion line 623
  23. def OAI.EuclideanFiveColor.CompactFunctions.compactSigma line 655
  24. lemma OAI.EuclideanFiveColor.CompactFunctions.compactSigma_le line 664
  25. lemma OAI.EuclideanFiveColor.CompactFunctions.measurable_compactSigma line 669
  26. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_simple line 687
  27. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_of_measurable_compactSigma line 706
  28. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_base line 725
  29. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_shift line 753
  30. lemma OAI.EuclideanFiveColor.CompactFunctions.measurable_shift_compactSigma line 763
  31. lemma OAI.EuclideanFiveColor.CompactFunctions.measurable_base_compactSigma line 775
  32. lemma OAI.EuclideanFiveColor.CompactFunctions.compact_descend line 803

    Source documentation

    Conditional integration projects an ambient finite module to the actual new factor, without sacrificing its uniform coefficient or basis bounds.

    lemma compact_descend (μ : Measure X) [IsProbabilityMeasure μ]
    (π : X → Z) (hπ : Measurable π) (p : Z → Y) (hp : Measurable p)
    (hπcov : ∀ k : K, ∀ᵐ x ∂μ, π (k • x) = k • π x)
    (H : Z → ℂ) (hH : Measurable H) (D : ℝ) (_hD : 0 ≤ D)
    (hHD : ∀ z, ‖H z‖ ≤ D)
    (hc : Compact (K := K) μ (p ∘ π) (H ∘ π)) :
…

    Mentions: OAI.EuclideanFiveColor.CompactFunctions.Compact