WIP: start proof of mulEquivHaarChar_prodCongr (#520)

[js2357]

This is my attempt at the beginning of the proof (#520), through the proof that ν is a Haar measure.

I think the proof in the blueprint is implicitly assuming that the groups involved are Hausdorff. Without that, the compact sets X and Y (as defined in the blueprint proof) are not necessarily measurable, and the proof gets more complicated. But maybe I'm missing something, so any feedback is welcome.

[kbuzzard]

My take on this: in all the FLT-related applications everything is Hausdorff and second-countable. The code I write is "with mathlib in mind" so I attempt to prove things in "the correct generality" but I am certainly no expert in measure theory. There was a Zulip thread on this question here #maths > Product of Borel spaces @ 💬 (the source of the blueprint proof) where I'm sure people would be happy to discuss whether Hausdorffness is needed. At the end of the day (I've noticed this in many places in FLT) there is some trade-off between "prove the result in the generality in which it is true" vs "prove enough for FLT" and I'm not sure there is a hard and fast rule here.

[DavidLedvinka]

Heres what I have:

open Set in
@[to_additive MeasureTheory.addEquivAddHaarChar_prodCongr]
lemma mulEquivHaarChar_prodCongr {mG : MeasurableSpace G} [BorelSpace G]
    {mH :MeasurableSpace H} [BorelSpace H] (φ : G ≃ₜ* G) (ψ : H ≃ₜ* H) :
    letI : MeasurableSpace (G × H) := borel _
    haveI : BorelSpace (G × H) := ⟨rfl⟩
    mulEquivHaarChar (φ.prodCongr ψ) = mulEquivHaarChar φ * mulEquivHaarChar ψ := by
  let ℬ : MeasurableSpace (G × H) := borel _
  have : BorelSpace (G × H) := ⟨rfl⟩
  let ρ := haar (G := G × H)
  have hσ : mG.prod mH ≤ ℬ := prod_le_borel_prod
  obtain ⟨K₁, _⟩ := exists_positiveCompacts_subset (α := G) isOpen_univ univ_nonempty
  obtain ⟨K₂, _⟩ := exists_positiveCompacts_subset (α := H) isOpen_univ univ_nonempty
  obtain ⟨K₁', hK₁'⟩ :=
    exists_positiveCompacts_subset (α := G) (isOpen_interior (s := K₁)) K₁.interior_nonempty
  let ρ₁ := ((ρ.trim hσ).restrict (univ ×ˢ interior (K₂ : Set H))).fst
  have hρ₁ {s : Set G} (hs : MeasurableSet s) : ρ₁ s = ρ (s ×ˢ interior (K₂ : Set H)) := by
    dsimp [ρ₁, fst]
    rw [map_apply (by fun_prop)]
    rw [←prod_univ, Measure.restrict_apply, trim_measurableSet_eq, prod_inter_prod, inter_univ,
      univ_inter]
    all_goals measurability
  have : IsMulLeftInvariant ρ₁ :=
    { map_mul_left_eq_self g := by
        ext s hs
        have : MeasurableSet ((fun x ↦ g * x) ⁻¹' s) := hs.preimage (by fun_prop) -- measurability
        rw[map_apply (by fun_prop), hρ₁, hρ₁]
        nth_rw 2 [← map_mul_left_eq_self ρ ⟨g,1⟩]
        conv in fun x ↦ (g, 1) * x => change fun x ↦ ((g * ·) x.1, (1 * ·) x.2)
        conv in fun x ↦ 1 * x => simp
        rw [map_apply (by fun_prop)]
        rw[← prod_preimage_left]
        all_goals measurability
    }
  have ρ_pos : ρ ((interior (K₁' : Set G)) ×ˢ (interior (K₂ : Set H))) ≠ 0 :=
    IsOpenPosMeasure.open_pos _
      (isOpen_prod_iff'.mpr (Or.inl ⟨isOpen_interior, isOpen_interior⟩))
      (Nonempty.prod K₁'.interior_nonempty K₂.interior_nonempty)
  have ρ_fin : ρ (K₁ ×ˢ K₂) < ⊤ :=
    IsFiniteMeasureOnCompacts.lt_top_of_isCompact (K₁.isCompact.prod K₂.isCompact)
  have ρ₁_harr : IsHaarMeasure ρ₁ := by
    apply isHaarMeasure_of_isCompact_nonempty_interior ρ₁ K₁' K₁'.isCompact K₁'.interior_nonempty
    · contrapose! ρ_pos
      rw [← hρ₁ (by measurability), ← nonpos_iff_eq_zero]
      exact le_of_le_of_eq (measure_mono interior_subset) ρ_pos
    · rw [← lt_top_iff_ne_top]
      apply lt_of_le_of_lt (measure_mono hK₁')
      · rw[hρ₁ (by measurability)]
        refine lt_of_le_of_lt ?_ ρ_fin
        exact measure_mono (prod_subset_prod_iff.mpr (Or.inl ⟨interior_subset , interior_subset⟩))
  sorry

This defines $\nu$ as $\rho_1$ and proves its a Haar measure. I use open sets that are "two compacts deep" in place of the compact sets from the blueprint. It can probably be golfed a lot. I think the rest of the proof should be completable using hρ₁ and the fact that $\rho_1$ and $\rho$ are Haar measures as in the blueprint. Feel free to use some or all of this code!

[js2357]

Now mostly complete, aside from regularity.

Note that the proof in the blueprint uses ringHaarChar, which isn't defined until a later file, so I reworked the proof slightly to avoid it rather than reorganize things.