Fubini's for fin 2 -> R

Stream: maths

[Andrew Souther]

I'm working on the unit disc with @Heather Macbeth and @James Arthur, and we'd like to start with this definition:
def unit_disc : set (euclidean_space ℝ (fin 2)) := metric.ball 0 1.

Ideally, we hope to keep the whole proof inside of euclidean_space ℝ (fin 2). However, we expect to use Fubini's Theorem, and it seems docs#measure_theory.integral_prod can only handle ℝ × ℝ.

@Floris van Doorn, did you have any plans to work on Fubini's theorem for (fin 2) → ℝ? If not, we'll try to figure out some work-arounds.

[Floris van Doorn]

I haven't worked on Fubini's theorem for finitary products yet, since I don't know the most convenient statements in applications. There is definitely a lot of API missing from measure.pi to make this convenient.

I expect/hope that this particular statement should follow without too much effort by the measurable equivalence docs#measurable_equiv.pi_measurable_equiv_tprod and the fact that this map is measure-preserving (for that we probably need an extensionality lemma similar to docs#measure_theory.measure.prod_eq). Though there will be some annoyances along the way (for example, tprod ... will be definitionally equal to ℝ × ℝ × punit instead of ℝ × ℝ).

Though maybe "Fubini for fin 2" is the wrong theorem to formalize. Better would be to have something that is generally applicable. Now that I think about good ways to formalize Fubini, I'm thinking that we need to have a more general definition of measure.pi, that measures only a subspace, something like this:

import measure_theory.pi

open measure_theory measure_theory.measure
open_locale classical

variables {ι : Type*} {π : ι → Type*} [∀ i, measurable_space (π i)]
  {μ : ∀ i, measure (π i)} [∀ i, sigma_finite (μ i)]

instance measurable_space.finset_pi (s : finset ι) : measurable_space (Π i ∈ s, π i) := sorry

def measure.finset_pi (s : finset ι) (μ : ∀ i, measure (π i)) : measure (Π i ∈ s, π i) :=
let h : ∀ i, measure (π i) := μ in sorry

lemma lintegral_pi_eq_lintegral_finset_pi [fintype ι] (i : ι) (f : (Π i, π i) → ennreal)
  (hf : measurable f) : ∫⁻ x, f x ∂(measure.pi μ) =
  ∫⁻ x, f (λ i, x i (finset.mem_univ i)) ∂(measure.finset_pi finset.univ μ ) := sorry

/-- Tonelli for finitary product measures -/
-- Fubini will look similar
lemma lintegral_finset_pi_split (s t : finset ι) (h : t ⊆ s) (f : (Π i ∈ s, π i) → ennreal)
  (hf : measurable f) :
  ∫⁻ x, f x ∂(measure.finset_pi μ s) =
  ∫⁻ x, ∫⁻ y, f _ ∂(measure.finset_pi (s \ t) μ) ∂(measure.finset_pi t μ) :=
sorry

[Heather Macbeth]

In the short term, I think there are two possible workarounds for Andrew and James. One way would be as Floris suggests:

Floris van Doorn said:

I expect/hope that this particular statement should follow without too much effort by the measurable equivalence docs#measurable_equiv.pi_measurable_equiv_tprod and the fact that this map is measure-preserving (for that we probably need an extensionality lemma similar to docs#measure_theory.measure.prod_eq). Though there will be some annoyances along the way (for example, tprod ... will be definitionally equal to ℝ × ℝ × punit instead of ℝ × ℝ).

effectively, temporarily jumping from (fin 2) → ℝ to ℝ × ℝ during the Fubini step of the proof.

The alternative would be to work in ℝ × ℝ throughout, having defined a new (Euclidean) product metric on ℝ × ℝ, by analogy with docs#pi_Lp. Is there any harm (or, on the other hand, any longer-term benefit) in doing this, i.e., in writing a full file topology.metric_space.prod_Lp, which is a line-by-line port of pi_Lp?

[Floris van Doorn]

Yeah, the easiest short-term solution is indeed to do all measure theory in ℝ × ℝ. For prod I think we have all the facts that should make the proof smooth.

[Yury G. Kudryashov]

You can just deal with volume {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 < 1} without introducing normed_space structure.