OAI/NumberTheory/Ostmann/Arithmetic/BulkIntegrands.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Bounded measurable bulk integrands, including sharp gates

The sharp terminal windows need not be continuous. This small function space retains their actual values while providing the finite-measure operations used in the bulk comparison.

  1. structure OAI.Ostmann.BulkIntegrand line 16
  2. instance OAI.Ostmann.(instance at line 21) line 21
  3. theorem OAI.Ostmann.BulkIntegrand.ext line 23
  4. def OAI.Ostmann.BulkIntegrand.sub line 31
  5. theorem OAI.Ostmann.BulkIntegrand.integrable line 39
  6. theorem OAI.Ostmann.BulkIntegrand.slice_integrable line 45
  7. def OAI.Ostmann.BulkIntegrand.average line 52
  8. theorem OAI.Ostmann.BulkIntegrand.average_bound line 64
  9. theorem OAI.Ostmann.BulkIntegrand.average_sub line 70
  10. theorem OAI.Ostmann.BulkIntegrand.average_commute line 76
  11. def OAI.Ostmann.BulkIntegrand.averages line 96
  12. theorem OAI.Ostmann.BulkIntegrand.averages_sub line 101
  13. theorem OAI.Ostmann.BulkIntegrand.averages_bound line 108
  14. theorem OAI.Ostmann.BulkIntegrand.averages_commute line 123
  15. theorem OAI.Ostmann.BulkIntegrand.averages_comparison line 135

    Source documentation

    Pointwise product comparison, valid also for the original sharp windows.

    theorem BulkIntegrand.averages_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 : BulkIntegrand σ) (ε : σ → ℝ) (hε : ∀ i ∈ l, 0 ≤ ε i)
    (herr : ∀ i ∈ l, ∀ x, ‖f.average (μ i) i x - f.average (ν i) i x‖ ≤ ε i) :
    ∀ x, ‖f.averages μ l x - f.averages ν l x‖ ≤ 2 ^ l.length * (l.map ε).sum := by
…

    Mentions: OAI.Ostmann.BulkIntegrand