feat(measure_theory/constructions/pi): volume on α × α as a map of …

…volume on `fin 2 → α` (#9432)

src/data/equiv/fin.lean

@@ -42,6 +42,38 @@ def fin_two_equiv : fin 2 ≃ bool :=
     { rw ← fin.succ_zero_eq_one, refl }
   end⟩
 
+/-- `Π i : fin 2, α i` is equivalent to `α 0 × α 1`. See also `fin_two_arrow_equiv` for a
+non-dependent version and `prod_equiv_pi_fin_two` for a version with inputs `α β : Type u`. -/
+@[simps {fully_applied := ff}] def pi_fin_two_equiv (α : fin 2 → Type u) : (Π i, α i) ≃ α 0 × α 1 :=
+{ to_fun := λ f, (f 0, f 1),
+  inv_fun := λ p, fin.cons p.1 $ fin.cons p.2 fin_zero_elim,
+  left_inv := λ f, funext $ fin.forall_fin_two.2 ⟨rfl, rfl⟩,
+  right_inv := λ ⟨x, y⟩, rfl }
+
+/-- A product space `α × β` is equivalent to the space `Π i : fin 2, γ i`, where
+`γ = fin.cons α (fin.cons β fin_zero_elim)`. See also `pi_fin_two_equiv` and
+`fin_two_arrow_equiv`. -/
+@[simps {fully_applied := ff }] def prod_equiv_pi_fin_two (α β : Type u) :
+  α × β ≃ Π i : fin 2, @fin.cons _ (λ _, Type u) α (fin.cons β fin_zero_elim) i :=
+(pi_fin_two_equiv (fin.cons α (fin.cons β fin_zero_elim))).symm
+
+/-- The space of functions `fin 2 → α` is equivalent to `α × α`. See also `pi_fin_two_equiv` and
+`prod_equiv_pi_fin_two`. -/
+@[simps {fully_applied := ff}] def fin_two_arrow_equiv (α : Type*) : (fin 2 → α) ≃ α × α :=
+pi_fin_two_equiv (λ _, α)
+
+/-- `Π i : fin 2, α i` is order equivalent to `α 0 × α 1`. See also `order_iso.fin_two_arrow_equiv`
+for a non-dependent version. -/
+def order_iso.pi_fin_two_iso (α : fin 2 → Type u) [Π i, preorder (α i)] :
+  (Π i, α i) ≃o α 0 × α 1 :=
+{ to_equiv := pi_fin_two_equiv α,
+  map_rel_iff' := λ f g, iff.symm fin.forall_fin_two }
+
+/-- The space of functions `fin 2 → α` is order equivalent to `α × α`. See also
+`order_iso.pi_fin_two_iso`. -/
+def order_iso.fin_two_arrow_iso (α : Type*) [preorder α] : (fin 2 → α) ≃o α × α :=
+order_iso.pi_fin_two_iso (λ _, α)
+
 /-- The 'identity' equivalence between `fin n` and `fin m` when `n = m`. -/
 def fin_congr {n m : ℕ} (h : n = m) : fin n ≃ fin m :=
 (fin.cast h).to_equiv

src/data/fin.lean

@@ -240,19 +240,10 @@ attribute [simp] val_zero
 
 lemma zero_le (a : fin (n + 1)) : 0 ≤ a := zero_le a.1
 
+lemma zero_lt_one : (0 : fin (n + 2)) < 1 := nat.zero_lt_one
+
 lemma pos_iff_ne_zero (a : fin (n+1)) : 0 < a ↔ a ≠ 0 :=
-begin
-  split,
-  { rintros h rfl, exact lt_irrefl _ h, },
-  { rintros h,
-    apply (@pos_iff_ne_zero _ _ (a : ℕ)).mpr,
-    cases a,
-    rintro w,
-    apply h,
-    simp at w,
-    subst w,
-    refl, },
-end
+by rw [← coe_fin_lt, coe_zero, pos_iff_ne_zero, ne.def, ne.def, ext_iff, coe_zero]
 
 lemma eq_zero_or_eq_succ {n : ℕ} (i : fin (n+1)) : i = 0 ∨ ∃ j : fin n, i = j.succ :=
 begin
@@ -950,6 +941,15 @@ lemma exists_fin_succ {P : fin (n+1) → Prop} :
 ⟨λ ⟨i, h⟩, fin.cases or.inl (λ i hi, or.inr ⟨i, hi⟩) i h,
   λ h, or.elim h (λ h, ⟨0, h⟩) $ λ⟨i, hi⟩, ⟨i.succ, hi⟩⟩
 
+lemma forall_fin_one {p : fin 1 → Prop} : (∀ i, p i) ↔ p 0 := @unique.forall_iff (fin 1) _ p
+lemma exists_fin_one {p : fin 1 → Prop} : (∃ i, p i) ↔ p 0 := @unique.exists_iff (fin 1) _ p
+
+lemma forall_fin_two {p : fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
+forall_fin_succ.trans $ and_congr_right $ λ _, forall_fin_one
+
+lemma exists_fin_two {p : fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
+exists_fin_succ.trans $ or_congr_right exists_fin_one
+
 /--
 Define `C i` by reverse induction on `i : fin (n + 1)` via induction on the underlying `nat` value.
 This function has two arguments: `hlast` handles the base case on `C (fin.last n)`,
@@ -1810,6 +1810,16 @@ lemma eq_insert_nth_iff {i : fin (n + 1)} {x : α i} {p : Π j, α (i.succ_above
   q = i.insert_nth x p ↔ q i = x ∧ p = (λ j, q (i.succ_above j)) :=
 eq_comm.trans insert_nth_eq_iff
 
+lemma insert_nth_apply_below {i j : fin (n + 1)} (h : j < i) (x : α i)
+  (p : Π k, α (i.succ_above k)) :
+  i.insert_nth x p j = eq.rec_on (succ_above_cast_lt h) (p $ j.cast_lt _) :=
+by rw [insert_nth, succ_above_cases, dif_neg h.ne, dif_pos h]
+
+lemma insert_nth_apply_above {i j : fin (n + 1)} (h : i < j) (x : α i)
+  (p : Π k, α (i.succ_above k)) :
+  i.insert_nth x p j = eq.rec_on (succ_above_pred h) (p $ j.pred _) :=
+by rw [insert_nth, succ_above_cases, dif_neg h.ne', dif_neg h.not_lt]
+
 lemma insert_nth_zero (x : α 0) (p : Π j : fin n, α (succ_above 0 j)) :
   insert_nth 0 x p = cons x (λ j, _root_.cast (congr_arg α (congr_fun succ_above_zero j)) (p j)) :=
 begin

src/data/matrix/notation.lean

@@ -148,6 +148,12 @@ set.ext $ λ y, by simp [fin.exists_fin_succ, eq_comm]
 @[simp] lemma range_empty (u : fin 0 → α) : set.range u = ∅ :=
 set.range_eq_empty _
 
+@[simp] lemma vec_cons_const (a : α) : vec_cons a (λ k : fin n, a) = λ _, a :=
+funext $ fin.forall_fin_succ.2 ⟨rfl, cons_val_succ _ _⟩
+
+lemma vec_single_eq_const (a : α) : ![a] = λ _, a :=
+funext $ unique.forall_iff.2 rfl
+
 /-- `![a, b, ...] 1` is equal to `b`.
 
   The simplifier needs a special lemma for length `≥ 2`, in addition to

src/measure_theory/constructions/pi.lean

@@ -398,6 +398,36 @@ variable (μ)
 instance pi.sigma_finite : sigma_finite (measure.pi μ) :=
 (finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in) (λ _ _, id)).sigma_finite
 
+lemma {u} pi_fin_two_eq_map {α : fin 2 → Type u} {m : Π i, measurable_space (α i)}
+  (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] :
+  measure.pi μ = map (measurable_equiv.pi_fin_two α).symm ((μ 0).prod (μ 1)) :=
+begin
+  refine pi_eq (λ s hs, _),
+  rw [measurable_equiv.map_apply, fin.prod_univ_succ, fin.prod_univ_succ, fin.prod_univ_zero,
+    mul_one, ← measure.prod_prod (hs _) (hs _)]; [skip, apply_instance],
+  congr' 1,
+  ext ⟨a, b⟩,
+  simp [fin.forall_fin_succ, is_empty.forall_iff]
+end
+
+lemma {u} map_pi_fin_two {α : fin 2 → Type u} {m : Π i, measurable_space (α i)}
+  (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] :
+  map (measurable_equiv.pi_fin_two α) (measure.pi μ) = ((μ 0).prod (μ 1)) :=
+(measurable_equiv.pi_fin_two α).map_apply_eq_iff_map_symm_apply_eq.2 (pi_fin_two_eq_map μ).symm
+
+lemma prod_eq_map_fin_two_arrow {α : Type*} {m : measurable_space α} (μ ν : measure α)
+  [sigma_finite μ] [sigma_finite ν] :
+  μ.prod ν = map measurable_equiv.fin_two_arrow (measure.pi ![μ, ν]) :=
+begin
+  haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩,
+  exact (map_pi_fin_two ![μ, ν]).symm
+end
+
+lemma prod_eq_map_fin_two_arrow_same {α : Type*} {m : measurable_space α} (μ : measure α)
+  [sigma_finite μ] :
+  μ.prod μ = map measurable_equiv.fin_two_arrow (measure.pi $ λ _, μ) :=
+by rw [prod_eq_map_fin_two_arrow, matrix.vec_single_eq_const, matrix.vec_cons_const]
+
 lemma pi_eval_preimage_null {i : ι} {s : set (α i)} (hs : μ i s = 0) :
   measure.pi μ (eval i ⁻¹' s) = 0 :=
 begin
@@ -582,6 +612,7 @@ lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (v
   volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) :=
 measure.pi_closed_ball _ _ hr
 
+section fun_unique
 /-!
 ### Integral over `ι → α` with `[unique ι]`
 
@@ -630,4 +661,65 @@ lemma set_integral_fun_unique' (ι : Type*) [unique ι] [measure_space β] (f :
   ∫ y : ι → β in @function.eval ι (λ _, β) (default ι) ⁻¹' s, f (y (default ι)) = ∫ x in s, f x :=
 by convert set_integral_fun_unique_pi' ι volume f s
 
+end fun_unique
+
+section fin_two_arrow
+
+variables {β E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E]
+  [topological_space.second_countable_topology E] [borel_space E] [complete_space E]
+
+lemma integral_fin_two_arrow_pi {m : measurable_space β} (μ ν : measure β)
+  [sigma_finite μ] [sigma_finite ν] (f : (fin 2 → β) → E) :
+  ∫ y, f y ∂(measure.pi ![μ, ν]) = ∫ x, f ![x.1, x.2] ∂(μ.prod ν) :=
+begin
+  haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩,
+  rw [measure.pi_fin_two_eq_map, integral_map_equiv], refl
+end
+
+lemma integral_fin_two_arrow_pi' {m : measurable_space β} (μ ν : measure β) [sigma_finite μ]
+  [sigma_finite ν] (f : β × β → E) :
+  ∫ y : fin 2 → β, f (y 0, y 1) ∂(measure.pi ![μ, ν]) = ∫ x, f x ∂(μ.prod ν) :=
+by { rw [measure.prod_eq_map_fin_two_arrow, integral_map_equiv], refl }
+
+lemma integral_fin_two_arrow [measure_space β] [sigma_finite (volume : measure β)]
+  (f : (fin 2 → β) → E) :
+  ∫ y, f y = ∫ x : β × β, f ![x.1, x.2] :=
+by rw [volume_pi, measure.volume_eq_prod, ← integral_fin_two_arrow_pi, matrix.vec_single_eq_const,
+  matrix.vec_cons_const]
+
+lemma integral_fin_two_arrow' [measure_space β] [sigma_finite (volume : measure β)]
+  (f : β × β → E) :
+  ∫ y : fin 2 → β, f (y 0, y 1) = ∫ x, f x :=
+by rw [volume_pi, measure.volume_eq_prod, ← integral_fin_two_arrow_pi', matrix.vec_single_eq_const,
+  matrix.vec_cons_const]
+
+lemma set_integral_fin_two_arrow_pi {m : measurable_space β} (μ ν : measure β)
+  [sigma_finite μ] [sigma_finite ν] (f : (fin 2 → β) → E) (s : set (fin 2 → β)) :
+  ∫ y in s, f y ∂(measure.pi ![μ, ν]) =
+    ∫ x : β × β in (fin_two_arrow_equiv β).symm ⁻¹' s, f ![x.1, x.2] ∂(μ.prod ν) :=
+begin
+  haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩,
+  rw [measure.pi_fin_two_eq_map, set_integral_map_equiv], refl
+end
+
+lemma set_integral_fin_two_arrow_pi' {m : measurable_space β} (μ ν : measure β)
+  [sigma_finite μ] [sigma_finite ν] (f : β × β → E) (s : set (β × β)) :
+  ∫ y : fin 2 → β in fin_two_arrow_equiv β ⁻¹' s, f (y 0, y 1) ∂(measure.pi ![μ, ν]) =
+    ∫ x in s, f x ∂(μ.prod ν) :=
+by { rw [set_integral_fin_two_arrow_pi, equiv.symm_preimage_preimage], simp }
+
+lemma set_integral_fin_two_arrow [measure_space β] [sigma_finite (volume : measure β)]
+  (f : (fin 2 → β) → E) (s : set (fin 2 → β)) :
+  ∫ y in s, f y = ∫ x in (fin_two_arrow_equiv β).symm ⁻¹' s, f ![x.1, x.2] :=
+by rw [measure.volume_eq_prod, ← set_integral_fin_two_arrow_pi, volume_pi,
+  matrix.vec_single_eq_const, matrix.vec_cons_const]
+
+lemma set_integral_fin_two_arrow' [measure_space β] [sigma_finite (volume : measure β)]
+  (f : β × β → E) (s : set (β × β)) :
+  ∫ y : fin 2 → β in fin_two_arrow_equiv β ⁻¹' s, f (y 0, y 1) = ∫ x in s, f x :=
+by rw [measure.volume_eq_prod, ← set_integral_fin_two_arrow_pi', volume_pi,
+  matrix.vec_single_eq_const, matrix.vec_cons_const]
+
+end fin_two_arrow
+
 end measure_theory

src/measure_theory/measurable_space.lean

@@ -7,7 +7,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import measure_theory.measurable_space_def
 import measure_theory.tactic
 import data.tprod
-
+import data.equiv.fin
 
 /-!
 # Measurable spaces and measurable functions
@@ -960,6 +960,17 @@ noncomputable def pi_measurable_equiv_tprod {l : list δ'} (hnd : l.nodup) (h :
   measurable_to_fun := measurable_pi_apply _,
   measurable_inv_fun := measurable_pi_iff.2 $ λ b, measurable_id }
 
+/-- The space `Π i : fin 2, α i` is measurably equivalent to `α 0 × α 1`. -/
+@[simps {fully_applied := ff}] def pi_fin_two (α : fin 2 → Type*) [∀ i, measurable_space (α i)] :
+  (Π i, α i) ≃ᵐ α 0 × α 1 :=
+{ to_equiv := pi_fin_two_equiv α,
+  measurable_to_fun := measurable.prod (measurable_pi_apply _) (measurable_pi_apply _),
+  measurable_inv_fun := measurable_pi_iff.2 $
+    fin.forall_fin_two.2 ⟨measurable_fst, measurable_snd⟩ }
+
+/-- The space `fin 2 → α` is measurably equivalent to `α × α`. -/
+@[simps {fully_applied := ff}] def fin_two_arrow : (fin 2 → α) ≃ᵐ α × α := pi_fin_two (λ _, α)
+
 end measurable_equiv
 
 namespace filter