# Zulip Chat Archive

## Stream: maths

### Topic: Fubini's for fin 2 -> R

#### Andrew Souther (Jan 09 2021 at 23:17):

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 (Jan 10 2021 at 00:18):

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 (Jan 10 2021 at 01:13):

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 (Jan 10 2021 at 09:43):

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 (Jan 11 2021 at 03:29):

You can just deal with `volume {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 < 1}`

without introducing `normed_space`

structure.

Last updated: May 14 2021 at 19:21 UTC