OAI/MeasureTheory/CompactFactors/Kernels.lean

GitHub source file

34 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. lemma OAI.EuclideanFiveColor.KernelCompact.norm_integral_sq line 45
  2. def OAI.EuclideanFiveColor.KernelCompact.fiberMean line 64
  3. lemma OAI.EuclideanFiveColor.KernelCompact.measurable_fiberMean line 67
  4. lemma OAI.EuclideanFiveColor.KernelCompact.fiberMean_bound line 71
  5. lemma OAI.EuclideanFiveColor.KernelCompact.fiberMean_l2_bound line 78
  6. lemma OAI.EuclideanFiveColor.KernelCompact.kernel_apply_error_bound line 108
  7. abbrev OAI.EuclideanFiveColor.RectangleDensity.Code line 161
  8. def OAI.EuclideanFiveColor.RectangleDensity.code line 163
  9. lemma OAI.EuclideanFiveColor.RectangleDensity.measurable_code line 168
  10. def OAI.EuclideanFiveColor.RectangleDensity.pairCode line 174
  11. lemma OAI.EuclideanFiveColor.RectangleDensity.measurable_pairCode line 176
  12. lemma OAI.EuclideanFiveColor.RectangleDensity.pairCode_mono line 179
  13. lemma OAI.EuclideanFiveColor.RectangleDensity.pairCode_generates line 187
  14. theorem OAI.EuclideanFiveColor.RectangleDensity.bounded_rectangles line 223

    Source documentation

    Bounded finite rectangle approximation for any probability coupling, not only a product measure. The common sup bound is twice the original bound.

    theorem bounded_rectangles (ν : Measure (X × Y)) [IsProbabilityMeasure ν]
    (L : X × Y → ℂ) (hL : Measurable L) (C : ℝ) (hC : 0 ≤ C)
    (hLC : ∀ z, ‖L z‖ ≤ C) (ε : ℝ) (hε : 0 < ε) :
    ∃ (n : ℕ) (a : Code n × Code n → ℂ),
      (∀ z, ‖a z‖ ≤ 2*C) ∧
      Integrable (fun z => ‖L z - a (pairCode n z)‖^2) ν ∧
      (∫ z, ‖L z - a (pairCode n z)‖^2 ∂ν) < ε^2 := by
…

    Mentions: OAI.EuclideanFiveColor.RectangleDensity.Code, OAI.EuclideanFiveColor.RectangleDensity.pairCode

  15. theorem OAI.EuclideanFiveColor.KernelCompact.bounded_range_approximation line 262

    Source documentation

    Uniform finite bounded-module approximation to the image of the bounded unit ball under an integral kernel. This is the compactness step of the relative compact-factor construction, with no spectral decomposition.

    theorem bounded_range_approximation (μ : Measure X) [IsProbabilityMeasure μ]
    (κ : Kernel Y X) [IsMarkovKernel κ] (q : X → Y) (hq : Measurable q)
    (L : X × X → ℂ) (hL : Measurable L) (C : ℝ) (hC : 0 ≤ C)
    (hLC : ∀ z, ‖L z‖ ≤ C) (ε : ℝ) (hε : 0 < ε) :
    ∃ (r : ℕ) (B C₀ : ℝ) (Hf : Fin r → X → ℂ),
      0 ≤ B ∧ 0 ≤ C₀ ∧ (∀ i, Measurable (Hf i)) ∧ (∀ x, ∑ i, ‖Hf i x‖ ≤ C₀) ∧
      ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ 1) →
        ∃ a : Y → Fin r → ℂ, Measurable a ∧ (∀ y, ‖a y‖ ≤ B) ∧
          Integrable (fun x => dist (∫ x', L (x,x') * f x' ∂κ (q x))
            (∑ i, a (q x) i * Hf i x)^2) μ ∧
          (∫ x, dist (∫ x', L (x,x') * f x' ∂κ (q x))
            (∑ i, a (q x) i * Hf i x)^2 ∂μ) < ε^2 := by
…
  16. def OAI.EuclideanFiveColor.KernelCompact.applyKernel line 354
  17. lemma OAI.EuclideanFiveColor.KernelCompact.applyKernel_covariance line 358
  18. lemma OAI.EuclideanFiveColor.KernelCompact.norm_sq_le_sub line 390
  19. theorem OAI.EuclideanFiveColor.KernelCompact.exists_nonzero_image line 397

    Source documentation

    A nonzero bounded relative-product kernel has a nonzero image of a bounded measurable function. Finite rectangle density replaces a spectral theorem.

    theorem exists_nonzero_image (μ : Measure X) [IsProbabilityMeasure μ]
    (κ : Kernel Y X) [IsMarkovKernel κ] (q : X → Y) (hq : Measurable q)
    (L : X × X → ℂ) (hL : Measurable L) (C : ℝ) (hC : 0 ≤ C)
    (hLC : ∀ z, ‖L z‖ ≤ C) (hne : ¬ L =ᵐ[μ ⊗ₘ κ.comap q hq] 0) :
    ∃ f : X → ℂ, Measurable f ∧ (∀ x, ‖f x‖ ≤ 1) ∧
      ¬ applyKernel κ q L f =ᵐ[μ] 0 := by
…

    Mentions: OAI.EuclideanFiveColor.KernelCompact.applyKernel

  20. lemma OAI.EuclideanFiveColor.KernelCompact.measurable_applyKernel line 475
  21. lemma OAI.EuclideanFiveColor.KernelCompact.applyKernel_bound line 481
  22. lemma OAI.EuclideanFiveColor.KernelCompact.exists_invariant_set line 492
  23. lemma OAI.EuclideanFiveColor.KernelCompact.indicator_not_constant line 503
  24. lemma OAI.EuclideanFiveColor.KernelCompact.row_constant line 528
  25. lemma OAI.EuclideanFiveColor.KernelCompact.centered_kernel line 554
  26. def OAI.EuclideanFiveColor.RelativeProduct.law line 619
  27. lemma OAI.EuclideanFiveColor.RelativeProduct.law_eq_mixture line 622
  28. lemma OAI.EuclideanFiveColor.RelativeProduct.law_swap line 640
  29. instance OAI.EuclideanFiveColor.RelativeProduct.law_probability line 658
  30. lemma OAI.EuclideanFiveColor.RelativeProduct.conditional_covariance line 663
  31. lemma OAI.EuclideanFiveColor.RelativeProduct.law_preserving line 673
  32. lemma OAI.EuclideanFiveColor.RelativeProduct.law_invariant line 707
  33. lemma OAI.EuclideanFiveColor.KernelCompact.image_conditional_mean_zero line 722
  34. lemma OAI.EuclideanFiveColor.KernelCompact.nonzero_not_factorizable line 753