OAI/NumberTheory/Ostmann/Tree/CoordinateAverages.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Successive averages in the real bulk coordinates

Finite measures act on bounded continuous functions by replacing one coordinate and integrating it. The operators commute at distinct coordinates, so a uniform one-coordinate error may be used before or after other replacements.

  1. def OAI.Ostmann.coordinateSlice line 17
  2. def OAI.Ostmann.coordinateAverage line 22
  3. theorem OAI.Ostmann.coordinateAverage_apply line 37
  4. theorem OAI.Ostmann.coordinateAverage_norm line 41
  5. theorem OAI.Ostmann.coordinateAverage_sub line 47
  6. theorem OAI.Ostmann.coordinateAverage_commute line 54
  7. def OAI.Ostmann.coordinateAverages line 72
  8. theorem OAI.Ostmann.coordinateAverages_sub line 77
  9. theorem OAI.Ostmann.coordinateAverages_norm line 84
  10. theorem OAI.Ostmann.coordinateAverages_commute line 97
  11. theorem OAI.Ostmann.coordinateAverages_comparison line 112

    Source documentation

    A uniform slice comparison accumulates only the masses of the other coordinates. It is applied to the original function, not assumed for functions which have already been averaged.

    theorem coordinateAverages_comparison {σ : Type*} [Fintype σ] (μ ν : σ → Measure ℝ)
    [∀ i, IsFiniteMeasure (μ i)] [∀ i, IsFiniteMeasure (ν i)]
    (l : List σ) (hl : l.Nodup)
    (hμ : ∀ i ∈ l, (μ i).real Set.univ ≤ 2)
    (hν : ∀ i ∈ l, (ν i).real Set.univ ≤ 2)
    (f : (σ → ℝ) →ᵇ ℂ) (ε : σ → ℝ) (hε : ∀ i ∈ l, 0 ≤ ε i)
    (herr : ∀ i ∈ l, ‖coordinateAverage (μ i) i f - coordinateAverage (ν i) i f‖ ≤ ε i) :
    ‖coordinateAverages μ l f - coordinateAverages ν l f‖ ≤
      2 ^ l.length * (l.map ε).sum := by
…

    Mentions: OAI.Ostmann.coordinateAverage, OAI.Ostmann.coordinateAverages