NestedAverage.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Products of nested conditional-average factors

Finite measurable partitions model the nested mesh inside one fixed root cell. Each factor is constant on the next partition and has average at most one on every current cell. The product estimate below is an actual integral estimate.

theorem OAI.LipschitzHilbert.integral_finite_profile_mul line 24

Source documentation

Decompose a finite-profile multiplier over its measurable cells.

theorem integral_finite_profile_mul (μ : Measure α) (P : α → κ)
    (hP : ∀ i, MeasurableSet {x | P x = i}) (c : κ → ℝ) (f : α → ℝ)
    (hf : Integrable f μ) :
    (∫ x, c (P x) * f x ∂μ) = ∑ i, c i * ∫ x in {x | P x = i}, f x ∂μ := by
…

theorem OAI.LipschitzHilbert.integral_finite_profile line 45
theorem OAI.LipschitzHilbert.integrable_finite_profile line 51

theorem OAI.LipschitzHilbert.integral_profile_mul_le line 69

Source documentation

Conditional cell-average domination contracts the integral of each nonnegative factor constant on the coarse partition.

theorem integral_profile_mul_le (μ : Measure α) [IsFiniteMeasure μ]
    (P : α → κ) (hP : ∀ i, MeasurableSet {x | P x = i})
    (c : κ → ℝ) (hc : ∀ i, 0 ≤ c i) (f : α → ℝ) (hf : Integrable f μ)
    (haverage : ∀ i, (∫ x in {x | P x = i}, f x ∂μ) ≤ μ.real {x | P x = i}) :
    (∫ x, c (P x) * f x ∂μ) ≤ ∫ x, c (P x) ∂μ := by
…

def OAI.LipschitzHilbert.nestedProductProfile line 78

Source documentation

The accumulated factor viewed as a function on its current partition.

def nestedProductProfile (R : ℕ → κ → κ) (g : ℕ → κ → ℝ) : ℕ → κ → ℝ
  | 0, _ => 1
  | n + 1, i => nestedProductProfile R g n (R n i) * g n i

omit [MeasurableSpace α] [Fintype κ] in

theorem OAI.LipschitzHilbert.nestedProductProfile_nonnegative line 83
theorem OAI.LipschitzHilbert.nestedProductProfile_eq_product line 95
theorem OAI.LipschitzHilbert.integrable_nested_product line 108

theorem OAI.LipschitzHilbert.nested_average_product_le line 122

Source documentation

Products of nonnegative next-step factors with conditional cell averages at most one have total integral at most the measure of the root space.

theorem nested_average_product_le (μ : Measure α) [IsFiniteMeasure μ]
    (P : ℕ → α → κ) (R : ℕ → κ → κ) (g : ℕ → κ → ℝ) (N : ℕ)
    (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}) :
    (∫ x, ∏ j ∈ Finset.range N, g j (P (j + 1) x) ∂μ) ≤ μ.real Set.univ := by
…

theorem OAI.LipschitzHilbert.nested_average_product_le_one line 152