OAI/Analysis/LipschitzHilbert/Estimates/WeightedAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.weighted_average_le line 18

   Source documentation

   A nonnegative factor of average at most one may be integrated against a weight comparable to a constant, with the same comparison loss.

   theorem weighted_average_le (μ : Measure α) [IsFiniteMeasure μ]
       (w f : α → ℝ) {c C : ℝ} (hc : 0 ≤ c) (hC : 0 ≤ C)
       (hw : AEStronglyMeasurable w μ) (hf : Integrable f μ)
       (hf0 : ∀ᵐ x ∂μ, 0 ≤ f x)
       (hlower : ∀ᵐ x ∂μ, c ≤ w x)
       (hupper : ∀ᵐ x ∂μ, w x ≤ C * c)
       (haverage : (∫ x, f x ∂μ) ≤ μ.real Set.univ) :
       Integrable (fun x => w x * f x) μ ∧
         (∫ x, w x * f x ∂μ) ≤ C * ∫ x, w x ∂μ := by
   …

2. theorem OAI.LipschitzHilbert.weighted_nested_average_le line 53

   Source documentation

   The actual product of nested normalized predictions admits the same weighted cell estimate.

   theorem weighted_nested_average_le [Fintype κ]
       (μ : Measure α) [IsFiniteMeasure μ]
       (P : ℕ → α → κ) (R : ℕ → κ → κ) (g : ℕ → κ → ℝ)
       (N : ℕ) (w : α → ℝ) {c C : ℝ} (hc : 0 ≤ c) (hC : 0 ≤ C)
       (hw : AEStronglyMeasurable w μ)
       (hlower : ∀ᵐ x ∂μ, c ≤ w x) (hupper : ∀ᵐ x ∂μ, w x ≤ C * c)
       (hP : ∀ n ≤ N, ∀ i, MeasurableSet {x | P n x = i})
       (hrefine : ∀ n < N, ∀ x, P n x = R n (P (n + 1) x))
       (hg : ∀ n < N, ∀ i, 0 ≤ g n i)
       (haverage : ∀ n < N, ∀ i,
         (∫ x in {x | P n x = i}, g n (P (n + 1) x) ∂μ) ≤ μ.real {x | P n x = i}) :
       Integrable (fun x => w x * ∏ j ∈ Finset.range N, g j (P (j + 1) x)) μ ∧
   …