OAI/NumberTheory/Ostmann/Arithmetic/BulkCoordinateEnumeration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulkCoordinateInsert_reindex line 11
2. theorem OAI.Ostmann.BulkIntegrand.selected_bulk_integral_enum line 30

   Source documentation

   The finite enumeration may be chosen for the proof while the product integral remains indexed by the original tree-and-word bulk coordinates.

   theorem BulkIntegrand.selected_bulk_integral_enum {σ J : Type*} [Fintype σ] [Fintype J]
       {k : ℕ} (f : BulkIntegrand σ) (base : σ → ℝ) (e : J ↪ σ) (g : Fin k ≃ J)
       (μ : σ → Measure ℝ) [∀ i, IsFiniteMeasure (μ i)] (y : J → ℝ) :
       f.averages μ ((List.finRange k).map (fun j => e (g j))) (bulkCoordinateInsert base e y) =
         ∫ z, f (bulkCoordinateInsert base e z) ∂Measure.pi (fun j => μ (e j)) := by
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.bulkCoordinateInsert