OAI/Analysis/FiniteFactor/ProductDensityLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.exists_limit_of_nested_inner line 14

   Source documentation

   Nested orthogonal projections with bounded squared norms converge strongly. For product densities, normalization supplies the displayed inner identity.

   theorem exists_limit_of_nested_inner {E : Type*} [NormedAddCommGroup E]
       [InnerProductSpace ℝ E] [CompleteSpace E] (f : ℕ → E) (C : ℝ)
       (hbound : ∀ n, ‖f n‖ ^ 2 ≤ C)
       (hinner : ∀ n m, n ≤ m → inner ℝ (f n) (f m) = ‖f n‖ ^ 2) :
       ∃ g : E, Tendsto f atTop (𝓝 g) ∧ ‖g‖ ^ 2 ≤ C := by
   …

2. theorem OAI.FiniteFactor.l2_norm_sq line 51
3. theorem OAI.FiniteFactor.l2_inner_toLp line 56
4. theorem OAI.FiniteFactor.l2_tendsto_setIntegral line 64
5. theorem OAI.FiniteFactor.exists_nonneg_L2_limit line 75

   Source documentation

   An actual nonnegative L2 function, obtained by completeness, with convergence of integrals on every measurable set. No limiting density is assumed.

   theorem exists_nonneg_L2_limit {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
       [IsFiniteMeasure μ] (f : ℕ → Ω → ℝ) (hf : ∀ n, MemLp (f n) 2 μ)
       (hnon : ∀ n, ∀ᵐ x ∂μ, 0 ≤ f n x) (C : ℝ)
       (hbound : ∀ n, (∫ x, f n x ^ 2 ∂μ) ≤ C)
       (hinner : ∀ n m, n ≤ m → (∫ x, f n x * f m x ∂μ) = ∫ x, f n x ^ 2 ∂μ) :
       ∃ g : Ω → ℝ, MemLp g 2 μ ∧ (∀ᵐ x ∂μ, 0 ≤ g x) ∧
         (∫ x, g x ^ 2 ∂μ) ≤ C ∧
         ∀ S, MeasurableSet S →
           Tendsto (fun n => ∫ x in S, f n x ∂μ) atTop (𝓝 (∫ x in S, g x ∂μ)) := by
   …