FLT/HaarMeasure/HaarChar/RealComplex.lean

GitHub source file

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

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

4 declarations, 0 contain sorry, 0 declared as axioms

The distributive Haar characters of ℝ and ℂ

This file computes ringHaarChar for ℝ and ℂ.

This lets us know what volume (x • s) is in terms of ‖x‖ and volume s, when x is a nonzero real/complex number and s is a set of reals/complex numbers.

Main declarations

Imports (8)
Imported by 3 files
  1. lemma Real.volume_real_smul line 39 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Set, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, HSMul.hSMul, HMul.hMul, NNNorm.nnnorm

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ENNReal.ofReal, abs, HPow.hPow, Nat, Module.finrank, MeasureTheory.Measure.addHaar_smul, ENorm.enorm, OfNat.ofNat, Module.finrank_self, pow_one, eq_self

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  2. lemma MeasureTheory.ringHaarChar_real The distributive Haar character of the action of ℝˣ on ℝ is the usual norm line 46 source

    Source documentation

    The distributive Haar character of the action of ℝˣ on ℝ is the usual norm.

    This means that volume (x • s) = ‖x‖ * volume s for all x : ℝ and s : Set ℝ. See Real.volume_real_smul.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Units, Real, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, NNNorm.nnnorm

    Proof uses: MeasureTheory.ringHaarChar_eq_of_measure_smul_eq_mul, MeasureTheory.MeasureSpace.volume, Set.Icc, OfNat.ofNat, LT.lt.ne', ENNReal, MeasureTheory.Measure, Set, MeasureTheory.Measure.measure_pos_of_nonempty_interior, of_eq_true, Set.Nonempty, interior, Eq.trans, LT.lt, True, Set.Ioo, congrArg, interior_Icc, IsCompact.measure_ne_top, CompactIccSpace.isCompact_Icc and 1 more

    113 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    lemma MeasureTheory.ringHaarChar_real (x : ℝˣ) : ringHaarChar x = ‖(x : ℝ)‖₊ :=
…

    Mentions: MeasureTheory.ringHaarChar

  3. lemma MeasureTheory.ringHaarChar_complex The distributive Haar character of the action of ℂˣ on ℂ is the usual norm squared line 56 source

    Source documentation

    The distributive Haar character of the action of ℂˣ on ℂ is the usual norm squared.

    This means that volume (z • s) = ‖z‖ ^ 2 * volume s for all z : ℂ and s : Set ℂ. See Complex.volume_complex_smul.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Units, Complex, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, HPow.hPow, Nat, NNNorm.nnnorm, OfNat.ofNat

    Proof uses: MeasureTheory.ringHaarChar_eq_of_measure_smul_eq_mul, MeasureTheory.MeasureSpace.volume, Complex.reProdIm, Set.Icc, Real, LT.lt.ne', ENNReal, MeasureTheory.Measure, Set, MeasureTheory.Measure.measure_pos_of_nonempty_interior, of_eq_true, Set.Nonempty, interior, Eq.trans, And, Set.Ioo, True, congrArg, Complex.interior_reProdIm, congr and 63 more

    298 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

    lemma MeasureTheory.ringHaarChar_complex (z : ℂˣ) : ringHaarChar z = ‖(z : ℂ)‖₊ ^ 2 := by
…

    Mentions: MeasureTheory.ringHaarChar

  4. lemma Complex.volume_complex_smul line 74 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Complex, Set, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, HSMul.hSMul, HMul.hMul, HPow.hPow, Nat, NNNorm.nnnorm, OfNat.ofNat

    Proof uses: Ne, Or, eq_or_ne, of_eq_true, Eq.trans, True, congr, congrArg, MeasurableSpace, Zero, SMulWithZero, MeasureTheory.NullSingletonClass, Set.Finite.measure_zero, Set.Finite.subset, Set.finite_zero, Set.zero_smul_set_subset, Real, congrFun', NNReal, nnnorm_zero and 21 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.