OAI/NumberTheory/Ostmann/ZeroDensity/BulkProductDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_pi_withDensity line 14

   Source documentation

   The scalar-density factors of the ideal bulk laws multiply inside one finite product integral. This is used with the nonnegative Page densities.

   theorem bulk_pi_withDensity {J : Type*} [Fintype J]
       (μ : J → Measure ℝ) [∀ j, IsFiniteMeasure (μ j)]
       (ρ : J → ℝ → ℝ)
       (hi : ∀ j, Integrable (ρ j) (μ j)) (hpos : ∀ j x, 0 ≤ ρ j x) :
       Measure.pi (fun j => (μ j).withDensity (fun x => ENNReal.ofReal (ρ j x))) =
         (Measure.pi μ).withDensity (fun x => ENNReal.ofReal (∏ j, ρ j (x j))) := by
   …

2. theorem OAI.Ostmann.bulk_integral_product_density line 44

   Source documentation

   Exact complex integral form of the joint density identity.

   theorem bulk_integral_product_density {J : Type*} [Fintype J]
       (μ : J → Measure ℝ) [∀ j, IsFiniteMeasure (μ j)]
       (ρ : J → ℝ → ℝ) (hρ : ∀ j, Measurable (ρ j))
       (hi : ∀ j, Integrable (ρ j) (μ j)) (hpos : ∀ j x, 0 ≤ ρ j x)
       (f : (J → ℝ) → ℂ) :
       (∫ x, f x ∂Measure.pi (fun j => (μ j).withDensity (fun y => ENNReal.ofReal (ρ j y)))) =
         ∫ x, f x * ((∏ j, ρ j (x j) : ℝ) : ℂ) ∂Measure.pi μ := by
   …