OAI/MeasureTheory/CompactFactors/ConditionalLimits.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EuclideanFiveColor.LimitDensity.clip line 45
2. lemma OAI.EuclideanFiveColor.LimitDensity.clip_bound line 46
3. lemma OAI.EuclideanFiveColor.LimitDensity.clip_eq line 49
4. lemma OAI.EuclideanFiveColor.LimitDensity.continuous_clip line 52
5. theorem OAI.EuclideanFiveColor.LimitDensity.bounded_vector_approximation line 58

   Source documentation

   A bounded vector measurable for a generated join is an L² limit of uniformly bounded functions measurable at finite stages.

   theorem bounded_vector_approximation
       (ν : Measure Y) [IsProbabilityMeasure ν] (ℱ : Filtration ℕ mY)
       (m : ℕ) (H : Y → Fin m → ℂ) (hH : Measurable[⨆ n, ℱ n] H)
       (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ y, ‖H y‖ ≤ C) :
       ∃ Hn : ℕ → Y → Fin m → ℂ,
         (∀ n, Measurable[ℱ n] (Hn n)) ∧
         (∀ n y, ‖Hn n y‖ ≤ 2*C) ∧
         (∀ n, Integrable (fun y => dist (H y) (Hn n y)^2) ν) ∧
         Tendsto (fun n => ∫ y, dist (H y) (Hn n y)^2 ∂ν) atTop (𝓝 0) := by
   …

6. theorem OAI.EuclideanFiveColor.LimitDensity.generated_factor_approximation line 141

   Source documentation

   At a generated limit factor, one earlier factor carries a bounded finite-vector approximant, with a pointwise bounded measurable representative.

   theorem generated_factor_approximation
       {Z : ℕ → Type*} [∀ n, MeasurableSpace (Z n)]
       (ν : Measure Y) [IsProbabilityMeasure ν] (p : ∀ n, Y → Z n)
       (hp : ∀ n, Measurable (p n))
       (hmono : Monotone (fun n => (inferInstance : MeasurableSpace (Z n)).comap (p n)))
       (hgen : (⨆ n, (inferInstance : MeasurableSpace (Z n)).comap (p n)) = mY)
       (m : ℕ) (H : Y → Fin m → ℂ) (hH : Measurable H)
       (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ y, ‖H y‖ ≤ C)
       (ε : ℝ) (hε : 0 < ε) :
       ∃ n, ∃ H₀ : Z n → Fin m → ℂ, Measurable H₀ ∧ (∀ z, ‖H₀ z‖ ≤ 2*C) ∧
         Integrable (fun y => dist (H y) (H₀ (p n y))^2) ν ∧
         (∫ y, dist (H y) (H₀ (p n y))^2 ∂ν) < ε^2 := by
   …

7. lemma OAI.PlaneFiveColor.Spectral.bounded_phase_encoding line 189
8. lemma OAI.PlaneFiveColor.Spectral.finite_encoding_at_of_approximation line 218
9. theorem OAI.PlaneFiveColor.Spectral.relative_singularity_limit line 269

   Source documentation

   The source limit implication: a generated increasing sequence of earlier compact successor factors supplies the requisite single approximation precision. The induction hypothesis is universal in the recentered wild map.

   theorem relative_singularity_limit
       {Z W : ℕ → Type*} [∀ n, MeasurableSpace (Z n)] [∀ n, MeasurableSpace (W n)]
       [∀ n, StandardBorelSpace (W n)] [∀ n, Nonempty (W n)]
       [∀ n, MulAction K (Z n)] [∀ n, MulAction K (W n)]
       [∀ n, MeasurableConstSMul K (Z n)] [∀ n, MeasurableConstSMul K (W n)]
       (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul K X μ]
       (d : X → D) (p : X → Y) (v : ∀ n, Y → Z n) (q : ∀ n, Z n → W n)
       (hd : Measurable d) (hp : Measurable p)
       (hv : ∀ n, Measurable (v n)) (hq : ∀ n, Measurable (q n))
       (hde : ∀ k : K, ∀ᵐ x ∂μ, d (k • x) = k • d x)
       (hpe : ∀ k : K, ∀ᵐ x ∂μ, p (k • x) = k • p x)
       (hve : ∀ n, ∀ k : K, ∀ᵐ y ∂μ.map p, v n (k • y) = k • v n y)
   …

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

10. lemma OAI.EuclideanFiveColor.ConditionalBase.condDistrib_given_const line 331
11. lemma OAI.EuclideanFiveColor.ConditionalBase.prod_given_const line 338
12. lemma OAI.PlaneFiveColor.Spectral.relative_singularity_base line 352
13. def OAI.PlaneFiveColor.Spectral.AmbientEncodingAt line 369
14. theorem OAI.PlaneFiveColor.Spectral.ambient_uniform_precision_contradiction line 385
15. lemma OAI.EuclideanFiveColor.CompactApproximation.scalar_identity line 556
16. lemma OAI.PlaneFiveColor.Spectral.ambient_encoding_of_at line 583
17. theorem OAI.PlaneFiveColor.Spectral.relative_singularity_approximation line 622

    Source documentation

    Relative singularity is closed under L² approximation by earlier factors, with all comparisons made on the ambient probability space. This form avoids choosing exactly commuting representatives at a countable tower join.

    theorem relative_singularity_approximation
        (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul K X μ]
        (d : X → D) (p : X → Y) (hd : Measurable d) (hp : Measurable p)
        (hde : ∀ k : K, ∀ᵐ x ∂μ, d (k • x) = k • d x)
        (hpe : ∀ k : K, ∀ᵐ x ∂μ, p (k • x) = k • p x)
        (hwild : IsWild (μ.map d))
        (ha : ∀ (m : ℕ) (H : Y → Fin m → ℂ), Measurable H →
          (∃ A : ℝ, ∀ y, ‖H y‖ ≤ A) → ∀ ε : ℝ, 0 < ε →
          ∃ q : X → W, Measurable q ∧
            (∀ k : K, ∀ᵐ x ∂μ, q (k • x) = k • q x) ∧
            (∀ b : X → D, Measurable b →
              (∀ k : K, ∀ᵐ x ∂μ, b (k • x) = k • b x) → IsWild (μ.map b) →
    …

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

18. def OAI.PlaneFiveColor.Spectral.UniversalGood line 669
19. lemma OAI.PlaneFiveColor.Spectral.universalGood_of_factor line 673