OAI/NumberTheory/Ostmann/Arithmetic/BulkPiIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The joint bulk integral in ordinary finite product coordinates

  1. def OAI.Ostmann.BulkIntegrand.headSlice line 13
  2. theorem OAI.Ostmann.fin_cons_update line 24
  3. theorem OAI.Ostmann.BulkIntegrand.headSlice_average line 36
  4. theorem OAI.Ostmann.BulkIntegrand.headSlice_averages line 44
  5. theorem OAI.Ostmann.BulkIntegrand.integral_headSlice line 54

    Source documentation

    Finite-measure Fubini, with the first coordinate displayed explicitly.

    theorem BulkIntegrand.integral_headSlice {n : ℕ} (f : BulkIntegrand (Fin (n + 1)))
    (μ : Fin (n + 1) → Measure ℝ) [∀ i, IsFiniteMeasure (μ i)] :
    (∫ x, f x ∂Measure.pi μ) =
      ∫ a, ∫ x, f.headSlice a x ∂Measure.pi (fun i => μ i.succ) ∂μ 0 := by
…

    Mentions: OAI.Ostmann.BulkIntegrand

  6. theorem OAI.Ostmann.BulkIntegrand.averages_finRange line 71