OAI/Analysis/LipschitzHilbert/Trees/SourceWindowAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Convert the constructed probability-normalized source factors to Lebesgue cell averages on the exact local line windows.

  1. theorem OAI.LipschitzHilbert.FiniteLineGrid.window_probability line 13
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.window_integrable_iff line 20
  3. theorem OAI.LipschitzHilbert.FiniteLineGrid.window_probability_integral line 27
  4. theorem OAI.LipschitzHilbert.FiniteLineGrid.window_average_le line 35

    Source documentation

    The constructed normalized factor has the required ordinary cell average, with the half-open source window retained exactly.

    theorem window_average_le (g : FiniteLineGrid) (F : ℝ → ℝ)
    (hint : Integrable F (intervalProbability g.origin (g.origin+g.width)))
    (havg : (∫ x, F x ∂intervalProbability g.origin (g.origin+g.width)) ≤ 1) :
    IntegrableOn F g.root volume ∧
      (∫ x in g.root, F x) ≤ volume.real g.root := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.intervalProbability