AddEquiv.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

11 declarations, 0 contain sorry, 0 declared as axioms

The Haar character under continuous group equivalences

We compute the Haar character mulEquivHaarChar of a continuous group equivalence and record its naturality under continuous additive/multiplicative isomorphisms and open embeddings.

Imports (6)

Imported by 7 files

lemma MeasureTheory._root_.ContinuousMulEquiv.isHaarMeasure_comap line 32 source
lemma MeasureTheory.mulEquivHaarChar_map_open Version of mulEquivHaarChar_smul_map without the regularity assumption In this case, the measures need only be equal on open sets line 47 source
Source comment
Version of `mulEquivHaarChar_smul_map` without the regularity assumption In this case, the measures need only be equal on open sets

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, MeasurableSpace, BorelSpace, IsTopologicalGroup, LocallyCompactSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsHaarMeasure, ContinuousMulEquiv, Set, IsOpen, Eq, ENNReal, HSMul.hSMul, NNReal, MeasureTheory.mulEquivHaarChar, MeasureTheory.Measure.map
Proof uses: Eq.mpr, MeasureTheory.Measure.haarScalarFactor, MeasureTheory.Measure.haar, id, congrArg, MeasureTheory.mulEquivHaarChar.eq_1, MeasureTheory.Measure.smul_apply, HMul.hMul, Classical.arbitrary, TopologicalSpace.PositiveCompacts, MeasureTheory.Measure.haarScalarFactor_eq_mul, mul_comm, SemigroupAction.mul_smul, Eq.symm, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isOpen, MeasureTheory.Measure.haarScalarFactor_map, OfNat.ofNat, MeasureTheory.Measure.haarScalarFactor_self, one_smul, Eq.refl
67 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma mulEquivHaarChar_map_open (μ : Measure G)
    [IsHaarMeasure μ] (φ : G ≃ₜ* G) {s : Set G} (hs : IsOpen s) :
    ((mulEquivHaarChar φ) • map φ μ) s = μ s := by
…
```
lemma MeasureTheory.mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsTopologicalGroup, LocallyCompactSpace, MeasurableSpace, BorelSpace, MonoidHom, Topology.IsOpenEmbedding, ContinuousMulEquiv, Eq, NNReal, MeasureTheory.mulEquivHaarChar
Proof uses: MeasureTheory.Measure, MeasureTheory.Measure.haar, MeasureTheory.Measure.comap, MeasureTheory.Measure.IsHaarMeasure, Topology.IsOpenEmbedding.isHaarMeasure_comap, Classical.arbitrary, TopologicalSpace.PositiveCompacts, MeasureTheory.Measure.Regular, MeasureTheory.Measure.Regular.comap', ContinuousMap, Real, And, HasCompactSupport, LE.le, OfNat.ofNat, Ne, Exists, exists_continuous_nonneg_pos, Continuous, ContinuousMap.mk and 37 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.mulEquivHaarChar_eq_mulEquivHaarChar_of_continuousMulEquiv line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsTopologicalGroup, LocallyCompactSpace, MeasurableSpace, BorelSpace, ContinuousMulEquiv, Eq, NNReal, MeasureTheory.mulEquivHaarChar
Proof uses: MeasureTheory.mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding, Homeomorph.isOpenEmbedding, ContinuousMulEquiv.toHomeomorph
19 instances, coercions and auxiliary constants left out.
def MeasureTheory._root_.ContinuousMulEquiv.prodCongr line 112 source
lemma MeasureTheory.mulEquivHaarChar_prodCongr line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, LocallyCompactSpace, MeasurableSpace, BorelSpace, SecondCountableTopologyEither, ContinuousMulEquiv, Eq, NNReal, MeasureTheory.mulEquivHaarChar, Prod, ContinuousMulEquiv.prodCongr, HMul.hMul
Proof uses: Exists, Set, And, Membership.mem, Filter, nhds, OfNat.ofNat, LE.le, Set.univ, IsCompact, local_compact_nhds, Filter.univ_mem, IsOpen, Iff.mp, mem_nhds_iff, SProd.sprod, IsOpen.prod, Set.image, Iff.mpr, Homeomorph and 108 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 100 steps
Open to load the checked before-and-after goal states.
def MeasureTheory._root_.ContinuousMulEquiv.piCongrRight line 240 source
lemma MeasureTheory.mulEquivHaarChar_piCongrRight line 256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, LocallyCompactSpace, MeasurableSpace, BorelSpace, SecondCountableTopology, Fintype, ContinuousMulEquiv, Eq, NNReal, MeasureTheory.mulEquivHaarChar, ContinuousMulEquiv.piCongrRight, Finset.prod, Finset.univ
Proof uses: Fintype.induction_subsingleton_or_nontrivial, Subsingleton, dite, Nonempty, Classical.propDecidable, Unique, Unique.mk', Classical.inhabited_of_nonempty, Eq.mpr, Inhabited.default, id, congrArg, Fintype.prod_subsingleton, MeasureTheory.mulEquivHaarChar_eq_mulEquivHaarChar_of_continuousMulEquiv, ContinuousMulEquiv.piUnique, rfl, Not, of_eq_true, Eq.trans, OfNat.ofNat and 31 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory._root_.WeaklyLocallyCompactSpace.of_isTopologicalGroup_of_isOpen_compactSpace_subgroup TODO this should be elsewhere note: it can't be an instance because typeclass inference can't find C line 296 source
Source comment
TODO this should be elsewhere note: it can't be an instance because typeclass inference can't find C
```
lemma _root_.WeaklyLocallyCompactSpace.of_isTopologicalGroup_of_isOpen_compactSpace_subgroup
    {A : Type*} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    (C : Subgroup A) [hCopen : Fact (IsOpen (C : Set A))] [CompactSpace C] :
    WeaklyLocallyCompactSpace A := .mk fun x ↦
…
```
lemma MeasureTheory.mulEquivHaarChar_restrictedProductCongrRight_of_principal line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, Subgroup, Fact, IsOpen, CompactSpace, Subtype, Membership.mem, MeasurableSpace, BorelSpace, LocallyCompactSpace, SecondCountableTopology, Set, Countable, LE.le, Filter, Filter.cofinite, Filter.principal, ContinuousMulEquiv and 10 more
Proof uses: Finite, Compl.compl, Fact.out, Set.Finite, Fintype, Set.Finite.fintype, ContinuousMulEquiv.symm, Set.BijOn.symm, And.intro, Set.LeftInvOn, Set.RightInvOn, ContinuousMulEquiv.apply_symm_apply, ContinuousMulEquiv.symm_apply_apply, ContinuousMulEquiv.mk, MulEquiv.mk, Equiv.mk, Set.MapsTo.restrict, Set.BijOn.mapsTo, Subtype.property, Subtype.ext and 53 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.mulEquivHaarChar_restrictedProductCongrRight line 368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, Subgroup, Fact, IsOpen, CompactSpace, Subtype, Membership.mem, MeasurableSpace, BorelSpace, LocallyCompactSpace, SecondCountableTopology, WeaklyLocallyCompactSpace, Countable, ContinuousMulEquiv, Filter.Eventually, Set.BijOn, Filter.cofinite, Eq and 5 more
Proof uses: Eq.mpr, id, congrArg, rfl, Set, Set.ofPred, LE.le, Filter, Filter.principal, Fact.mk, Iff.mpr, Filter.eventually_principal, MonoidHom, RestrictedProduct.mapAlongMonoidHom, Filter.Tendsto, Filter.tendsto_id', Fact.out, MonoidHom.id, Filter.Eventually.of_forall, Set.MapsTo and 5 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.