FiniteLineAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Products of the actual finer-cell step factors on a finite line grid.

theorem OAI.LipschitzHilbert.nonnegative_fiber_profile line 15

theorem OAI.LipschitzHilbert.FiniteLineGrid.integrable_product line 37

Source documentation

The actual finer-cell factors have a finite profile, so their product is integrable on every finite measure.

theorem integrable_product (g : FiniteLineGrid) (μ : Measure ℝ) [IsFiniteMeasure μ]
    (Γ : ℕ → ℝ → ℝ)
    (hΓ : ∀ n < g.depth, ∀ x, 0 ≤ Γ n x)
    (hconstant : ∀ n < g.depth, ∀ x y,
      g.index (n + 1) x = g.index (n + 1) y → Γ n x = Γ n y) :
    Integrable (fun x => ∏ n ∈ Finset.range g.depth, Γ n x) μ := by
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid

theorem OAI.LipschitzHilbert.FiniteLineGrid.average_product_le line 71

Source documentation

Finer-cell constancy and current-cell averages suffice for the actual line-grid product. The finite profiles are constructed from the step factors; the partition refinement is the proved floor-grid identity.

theorem average_product_le (g : FiniteLineGrid) (μ : Measure ℝ) [IsFiniteMeasure μ]
    (Γ : ℕ → ℝ → ℝ)
    (hΓ : ∀ n < g.depth, ∀ x, 0 ≤ Γ n x)
    (hconstant : ∀ n < g.depth, ∀ x y,
      g.index (n + 1) x = g.index (n + 1) y → Γ n x = Γ n y)
    (haverage : ∀ n < g.depth, ∀ i : Fin (g.branching ^ g.depth),
      (∫ x in {x | g.index n x = i}, Γ n x ∂μ) ≤
        μ.real {x | g.index n x = i}) :
    (∫ x, ∏ n ∈ Finset.range g.depth, Γ n x ∂μ) ≤ μ.real Set.univ := by
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid