Is this true by rfl?

I doesn't work for me

rfl?

I doesn't work for me

I think we might want t ∩ mk' x.val s.directionᗮ to be of type Set (mk' x.val s.directionᗮ), otherwise this theorem can't be applied to recursively decompose over different subspcaes.

Maybe this isn't as useful as I think though

Since the μHE is preserved through subspace inclusion, it is trivial to rewrite this to a set in the subspace, so I think there isn't much difference in strength in application between the two form.

I think in my later application I find this form more useful, where one states simplex.volume = 1/n*height*base without moving between subspaces.

Can't you prove this "by definition"? For instance going through Module.Basis.addHaar_eq_iff (there might be some missing API).

I tried a little bit, but couldn't get it shorter. The huge chunk of this proof (line 243 to line 250) is spent on transferring measure between different spaces (V and ℝ), and the only tool for this I have found is LinearIsometryEquiv.measurePreserving.

The missing API here is to generalize MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar to two different spaces, but the determinant will become basis-dependent. A possible statement might look like

map f b1.addHaar = ENNReal.ofReal |(f.toMatrix b1 b2).det⁻¹| • b2.addHaar

(didn't check carefully and I might have swapped the basis b1 and b2)
This looks like it is worth its separate PR

Wait, what I said doesn't sound right. I just found Module.Basis.map_addHaar. Let me try more

This is how far I have got

theorem MeasureTheory.volume_eq_of_finrank_eq_one {V : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
    [BorelSpace V] [FiniteDimensional ℝ V] (h : Module.finrank ℝ V = 1) {v : V} (hv : v ≠ 0) :
    (volume : Measure V) = ‖v‖ₑ • (volume : Measure ℝ).map (· • v) := by
  let f : ℝ ≃L[ℝ] V := (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (LinearEquiv.ofTop _ sorry).toContinuousLinearEquiv
  suffices (volume : Measure V) = ‖v‖ₑ • (volume : Measure ℝ).map f by
    simpa
  rw [← (stdOrthonormalBasis ℝ ℝ).addHaar_eq_volume, Module.Basis.map_addHaar]
  suffices ((stdOrthonormalBasis ℝ ℝ).toBasis.map f.toLinearEquiv).addHaar =
      ‖v‖₊⁻¹ • volume by
    simp [this]
    sorry
  rw [Module.Basis.addHaar_eq_iff]
  sorry

This is going longer than the current proof and I am not sure what is missing

Here is what I think would be a reasonable way:

theorem MeasureTheory.volume_eq_of_finrank_eq_one {V : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
    [BorelSpace V] [FiniteDimensional ℝ V] (h : Module.finrank ℝ V = 1) {v : V} (hv : v ≠ 0) :
    (volume : Measure V) = ‖v‖ₑ • (volume : Measure ℝ).map (· • v) := by
  let f : ℝ ≃L[ℝ] V := (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (LinearEquiv.ofTop _ sorry).toContinuousLinearEquiv
  suffices (volume : Measure V) = ‖v‖ₑ • (volume : Measure ℝ).map f by simpa
  change _ = ‖v‖₊ • volume.map f
  let b : OrthonormalBasis Unit ℝ V := sorry
  rw [← b.addHaar_eq_volume, Module.Basis.addHaar_eq_iff]
  rw [smul_apply, map_apply]
  · have : f ⁻¹' b.toBasis.parallelepiped = Set.Icc 0 ‖v‖⁻¹ := sorry
    rw [this, Real.volume_Icc]
    · sorry
  · fun_prop
  · exact (TopologicalSpace.PositiveCompacts.isCompact _).measurableSet

What is missing: creating an orthonormal basis from a single nonzero vector (similar to FiniteDimensional.basisSingleton), what does parallelepiped look like in dimension 1, and the last sorry is some ugly ENNReal computation which I think should be easy with tactics but isn't.

Thanks. I'll see what I can do with these missing pieces and will PR them if I get something good. For now, I am keeping the current proof here as it is not that long, even though not pretty. I don't think this should block the PR

PR for singleton basis: #37506

I am wondering whether it wouldn't be worth factoring this out as a separate lemma.

Do you mean the statement volume = ((volume : Measure ℝ).map (‖v‖⁻¹ • ·)).map (· • v)? This looks too niche to me to be a lemma

Can you open the EuclideanGeometry namespace? That would shorten some names inside proofs.

This ended up only shortening one, and I had to put the open statement in the middle of the file because there was no existing constant in this namespace from imports. I applied the suggestion anyway as this might be beneficial when I append this file with more lemma in the future