Lean Ridgelet Blueprint

4.3. Harmonic-analysis method: the affine Mackey model🔗

The affine group is the concrete instance that Theorem 2.5 of arXiv:2405.13682 needs, and it is also where the analysis is hardest. This chapter follows the Lean dependency order of the affine layer: the Jacobian and the two quasi-invariant L^2 representations, the explicit frequency action, the group and orbit input of the Mackey machine, the homogeneous-space model and its quasi-invariant character twist, the normalized-section realization of unitary induction, and the inducing fiber of the imprimitivity argument.

Theorem4.3.1
Statement uses 2
Statement dependency previews
Preview
Lemma 4.2.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 5
Reverse dependency previews
Preview
Theorem 4.3.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Concrete affine instance. Writing g(x)=Lx+t, the parameter action is the block lower-triangular map (a,b)\mapsto(L^{-T}a,b+\langle t,L^{-T}a\rangle). Its determinant is $(\det L)^{-1}. Additive Haar measure therefore has reciprocal data/parameter densities $\lVert\det L\rVert and \lVert\det L\rVert^{-1}; their square roots give both balance laws. The generic quasi-invariant construction now yields the two unitary L^2 representations and the synthesis/ridgelet Bochner intertwining identities for the affine feature.

Lean code for Theorem4.3.111 declarations
  • complete
    def LeanRidgelet.affineParameterLinearEquiv.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g : E ≃ᵃ[] E) : (E × ) ≃ₗ[] E × 
    def LeanRidgelet.affineParameterLinearEquiv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      (g : E ≃ᵃ[] E) : (E × ) ≃ₗ[] E × 
    Implementation after :=
    :=
      g.linear.symm.adjoint.skewProd (LinearEquiv.refl ℝ ℝ) (affineParameterShear g)
    The contragredient affine action on ridge parameters `(a, b)`. If `g x = L x + t`, this sends
    `(a, b)` to `(L⁻ᵀ a, b + ⟪t, L⁻ᵀ a⟫)`. 
  • theoremdefined in LeanRidgelet/HA/Affine.lean
    complete
    theorem LeanRidgelet.affineRidgeArgument_invariant.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g : E ≃ᵃ[] E) (x : E) (p : E × ) :
      LeanRidgelet.affineRidgeArgument (g x)
          ((LeanRidgelet.affineParameterLinearEquiv g) p) =
        LeanRidgelet.affineRidgeArgument x p
    theorem LeanRidgelet.affineRidgeArgument_invariant.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (g : E ≃ᵃ[] E)
      (x : E) (p : E × ) :
      LeanRidgelet.affineRidgeArgument (g x)
          ((LeanRidgelet.affineParameterLinearEquiv
              g)
            p) =
        LeanRidgelet.affineRidgeArgument x p
    The ridge argument is invariant under the joint affine data/parameter action. 
  • theoremdefined in LeanRidgelet/HA/Affine.lean
    complete
    theorem LeanRidgelet.det_affineParameterLinearEquiv.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g : E ≃ᵃ[] E) :
      LinearMap.det (LeanRidgelet.affineParameterLinearEquiv g) =
        (LinearMap.det g.linear)⁻¹
    theorem LeanRidgelet.det_affineParameterLinearEquiv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      (g : E ≃ᵃ[] E) :
      LinearMap.det
          (LeanRidgelet.affineParameterLinearEquiv
              g) =
        (LinearMap.det g.linear)⁻¹
    The parameter action has determinant `(det L)⁻¹`. 
  • complete
    def LeanRidgelet.affineDataJacobian.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (g : E ≃ᵃ[] E) :
      E  NNReal
    def LeanRidgelet.affineDataJacobian.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (g : E ≃ᵃ[] E) : E  NNReal
    Implementation after :=
    :=
      fun _ ↦ ‖LinearMap.det (g.linear : E →ₗ[ℝ] E)‖₊
    The constant Radon--Nikodym density for the inverse affine data action. 
  • complete
    def LeanRidgelet.affineParameterJacobian.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (g : E ≃ᵃ[] E) :
      E ×   NNReal
    def LeanRidgelet.affineParameterJacobian.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (g : E ≃ᵃ[] E) : E ×   NNReal
    Implementation after :=
    :=
      fun _ ↦ ‖LinearMap.det (g.linear : E →ₗ[ℝ] E)‖₊⁻¹
    The constant Radon--Nikodym density for the inverse contragredient parameter action. 
  • theoremdefined in LeanRidgelet/HA/Affine.lean
    complete
    theorem LeanRidgelet.affine_synthesis_radonNikodym_balance.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (g : E ≃ᵃ[] E) (x : E)
      (p : E × ) :
      (NNReal.sqrt (LeanRidgelet.affineParameterJacobian g p)) =
        LeanRidgelet.radonNikodymWeight LeanRidgelet.affineDataJacobian g x
    theorem LeanRidgelet.affine_synthesis_radonNikodym_balance.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] (g : E ≃ᵃ[] E)
      (x : E) (p : E × ) :
      (NNReal.sqrt
              (LeanRidgelet.affineParameterJacobian
                g p)) =
        LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineDataJacobian g x
    The synthesis balance in the form expected by the generic quasi-invariant theorem. 
  • theoremdefined in LeanRidgelet/HA/Affine.lean
    complete
    theorem LeanRidgelet.affine_ridgelet_radonNikodym_balance.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g : E ≃ᵃ[] E) (x : E) (p : E × ) :
      (NNReal.sqrt (LeanRidgelet.affineDataJacobian g x)) =
        LeanRidgelet.radonNikodymWeight LeanRidgelet.affineParameterJacobian
          g p
    theorem LeanRidgelet.affine_ridgelet_radonNikodym_balance.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (g : E ≃ᵃ[] E)
      (x : E) (p : E × ) :
      (NNReal.sqrt
              (LeanRidgelet.affineDataJacobian
                g x)) =
        LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineParameterJacobian
          g p
    The ridgelet balance in the form expected by the generic quasi-invariant theorem. 
  • complete
    def LeanRidgelet.affineDataLpUnitaryRepresentation.{u_1, u_2} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {Y : Type u_2}
      [NormedAddCommGroup Y] [InnerProductSpace  Y] [CompleteSpace Y]
      (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
      [MeasureTheory.SigmaFinite μ] :
      UnitaryRepresentation (E ≃ᵃ[] E) (MeasureTheory.Lp Y 2 μ)
    def LeanRidgelet.affineDataLpUnitaryRepresentation.{u_1,
        u_2}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {Y : Type u_2} [NormedAddCommGroup Y]
      [InnerProductSpace  Y]
      [CompleteSpace Y]
      (μ : MeasureTheory.Measure E)
      [μ.IsAddHaarMeasure]
      [MeasureTheory.SigmaFinite μ] :
      UnitaryRepresentation (E ≃ᵃ[] E)
        (MeasureTheory.Lp Y 2 μ)
    Implementation after :=
    :=
      quasiInvariantLpUnitaryRepresentation (E := Y) affineDataJacobian
        affineData_measurable (affineData_group_map_eq_withDensity μ)
        affineDataJacobian_measurable affineDataJacobian_ne_zero
        affineDataJacobian_one affineDataJacobian_cocycle
    The Radon--Nikodym-corrected affine data representation on Bochner `L²`. 
  • complete
    def LeanRidgelet.affineParameterLpUnitaryRepresentation.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (ν : MeasureTheory.Measure (E × ))
      [ν.IsAddHaarMeasure] [MeasureTheory.SigmaFinite ν] :
      UnitaryRepresentation (E ≃ᵃ[] E) (MeasureTheory.Lp  2 ν)
    def LeanRidgelet.affineParameterLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (ν : MeasureTheory.Measure (E × ))
      [ν.IsAddHaarMeasure]
      [MeasureTheory.SigmaFinite ν] :
      UnitaryRepresentation (E ≃ᵃ[] E)
        (MeasureTheory.Lp  2 ν)
    Implementation after :=
    :=
      quasiInvariantLpUnitaryRepresentation affineParameterJacobian
        affineParameter_measurable (affineParameter_group_map_eq_withDensity ν)
        affineParameterJacobian_measurable affineParameterJacobian_ne_zero
        affineParameterJacobian_one affineParameterJacobian_cocycle
    The Radon--Nikodym-corrected contragredient parameter representation on scalar `L²`. 
  • theoremdefined in LeanRidgelet/HA/Affine.lean
    complete
    theorem LeanRidgelet.affineBochnerSynthesis_intertwines.{u_1, u_2}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace  Y]
      [CompleteSpace Y] (ν : MeasureTheory.Measure (E × ))
      [ν.IsAddHaarMeasure] (σ :   Y) (g : E ≃ᵃ[] E) (γ : E ×   )
      (x : E) :
      LeanRidgelet.bochnerSynthesis ν (LeanRidgelet.affineFeature σ)
          (LeanRidgelet.quasiRegularAction
            (LeanRidgelet.radonNikodymWeight
              LeanRidgelet.affineParameterJacobian)
            g γ)
          x =
        LeanRidgelet.quasiUnitaryPullbackAction
          LeanRidgelet.affineDataJacobian 1 g
          (LeanRidgelet.bochnerSynthesis ν (LeanRidgelet.affineFeature σ) γ)
          x
    theorem LeanRidgelet.affineBochnerSynthesis_intertwines.{u_1,
        u_2}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {Y : Type u_2} [NormedAddCommGroup Y]
      [InnerProductSpace  Y]
      [CompleteSpace Y]
      (ν : MeasureTheory.Measure (E × ))
      [ν.IsAddHaarMeasure] (σ :   Y)
      (g : E ≃ᵃ[] E) (γ : E ×   )
      (x : E) :
      LeanRidgelet.bochnerSynthesis ν
          (LeanRidgelet.affineFeature σ)
          (LeanRidgelet.quasiRegularAction
            (LeanRidgelet.radonNikodymWeight
              LeanRidgelet.affineParameterJacobian)
            g γ)
          x =
        LeanRidgelet.quasiUnitaryPullbackAction
          LeanRidgelet.affineDataJacobian 1 g
          (LeanRidgelet.bochnerSynthesis ν
            (LeanRidgelet.affineFeature σ) γ)
          x
    The quasi-invariant Bochner synthesis identity instantiated for the affine fully-connected
    feature. 
  • theoremdefined in LeanRidgelet/HA/Affine.lean
    complete
    theorem LeanRidgelet.affineBochnerRidgelet_intertwines.{u_1, u_2} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {Y : Type u_2}
      [NormedAddCommGroup Y] [InnerProductSpace  Y] [CompleteSpace Y]
      (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ψ :   Y)
      (g : E ≃ᵃ[] E) (f : E  Y) (p : E × ) :
      LeanRidgelet.bochnerRidgelet μ (LeanRidgelet.affineFeature ψ)
          (LeanRidgelet.quasiUnitaryPullbackAction
            LeanRidgelet.affineDataJacobian 1 g f)
          p =
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight
            LeanRidgelet.affineParameterJacobian)
          g
          (LeanRidgelet.bochnerRidgelet μ (LeanRidgelet.affineFeature ψ) f)
          p
    theorem LeanRidgelet.affineBochnerRidgelet_intertwines.{u_1,
        u_2}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {Y : Type u_2} [NormedAddCommGroup Y]
      [InnerProductSpace  Y]
      [CompleteSpace Y]
      (μ : MeasureTheory.Measure E)
      [μ.IsAddHaarMeasure] (ψ :   Y)
      (g : E ≃ᵃ[] E) (f : E  Y)
      (p : E × ) :
      LeanRidgelet.bochnerRidgelet μ
          (LeanRidgelet.affineFeature ψ)
          (LeanRidgelet.quasiUnitaryPullbackAction
            LeanRidgelet.affineDataJacobian 1
            g f)
          p =
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight
            LeanRidgelet.affineParameterJacobian)
          g
          (LeanRidgelet.bochnerRidgelet μ
            (LeanRidgelet.affineFeature ψ) f)
          p
    The quasi-invariant Bochner ridgelet identity instantiated for the affine fully-connected
    feature. 
Theorem4.3.2
Statement uses 4
Statement dependency previews
Preview
Theorem 4.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

The explicit frequency action on all of . The contragredient action has reciprocal determinant density, so its corrected pullback is f(\xi)\mapsto |\det L|^{1/2}f(L^T\xi). Multiplication by the norm-one translation character is a second unitary operator. Their composite therefore exists directly on Lp classes and has the expected almost-everywhere representative. The Fourier covariance calculation first proves equality with the Plancherel conjugate on Schwartz functions; continuity and Schwartz density extend it to every class.

Lean code for Theorem4.3.214 declarations
  • complete
    def LeanRidgelet.affineDualAction.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g : E ≃ᵃ[] E) (xi : E) : E
    def LeanRidgelet.affineDualAction.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (g : E ≃ᵃ[] E)
      (xi : E) : E
    Implementation after :=
    := g.linear.symm.adjoint xi
    The affine group acts on frequency space through the contragredient of its linear part. 
  • complete
    def LeanRidgelet.affineDualJacobian.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (g : E ≃ᵃ[] E) :
      E  NNReal
    def LeanRidgelet.affineDualJacobian.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (g : E ≃ᵃ[] E) : E  NNReal
    Implementation after :=
    :=
      fun _ ↦ ‖LinearMap.det (g.linear : E →ₗ[ℝ] E)‖₊⁻¹
    The constant density of the inverse dual action. 
  • complete
    theorem LeanRidgelet.affineDualAction_map_eq_withDensity.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (g : E ≃ᵃ[] E) :
      MeasureTheory.Measure.map (LeanRidgelet.affineDualAction g⁻¹)
          MeasureTheory.volume =
        MeasureTheory.volume.withDensity fun xi 
          (LeanRidgelet.affineDualJacobian g xi)
    theorem LeanRidgelet.affineDualAction_map_eq_withDensity.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) :
      MeasureTheory.Measure.map
          (LeanRidgelet.affineDualAction g⁻¹)
          MeasureTheory.volume =
        MeasureTheory.volume.withDensity
          fun xi 
          (LeanRidgelet.affineDualJacobian g
              xi)
    Pushforward of Lebesgue measure by the inverse dual action. 
  • complete
    def LeanRidgelet.affineDualPullbackLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] :
      UnitaryRepresentation (E ≃ᵃ[] E)
        (MeasureTheory.Lp  2 MeasureTheory.volume)
    def LeanRidgelet.affineDualPullbackLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      UnitaryRepresentation (E ≃ᵃ[] E)
        (MeasureTheory.Lp  2
            MeasureTheory.volume)
    Implementation after :=
    := by
      letI : MulAction (E ≃ᵃ[ℝ] E) E := affineDualMulAction
      exact quasiInvariantLpUnitaryRepresentation affineDualJacobian
        (fun g ↦ affineDualAction_measurable g)
        (fun g ↦ affineDualAction_map_eq_withDensity g)
        affineDualJacobian_measurable affineDualJacobian_ne_zero
        affineDualJacobian_one (fun g h xi ↦ affineDualJacobian_cocycle g h xi)
    The determinant-corrected pullback representation for the contragredient action on frequency
    space. 
  • complete
    theorem LeanRidgelet.affineDualPullbackLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) (f : (MeasureTheory.Lp  2 MeasureTheory.volume)) :
      ((LeanRidgelet.affineDualPullbackLpUnitaryRepresentation g)
              f) =ᵐ[MeasureTheory.volume]
        fun xi 
        (NNReal.sqrt LinearMap.det g.linear‖₊) 
          f (g.linear.adjoint xi)
    theorem LeanRidgelet.affineDualPullbackLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E)
      (f :
        (MeasureTheory.Lp  2
            MeasureTheory.volume)) :
      ((LeanRidgelet.affineDualPullbackLpUnitaryRepresentation
                  g)
              f) =ᵐ[MeasureTheory.volume]
        fun xi 
        (NNReal.sqrt
                LinearMap.det g.linear‖₊) 
          f (g.linear.adjoint xi)
    The dual pullback representation acts by `|det L|¹ᐟ² f(Lᵀξ)` on every `L²` class. 
  • complete
    def LeanRidgelet.affineFrequencyPhase.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (g : E ≃ᵃ[] E)
      (xi : E) : 
    def LeanRidgelet.affineFrequencyPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] (g : E ≃ᵃ[] E)
      (xi : E) : 
    Implementation after :=
    :=
      ((Real.fourierChar (-⟪g 0, xi⟫_ℝ) : Circle) : ℂ)
    The translation character appearing in the Fourier-side affine action. 
  • complete
    theorem LeanRidgelet.affineFrequencyPhase_translation.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (b xi : E) :
      LeanRidgelet.affineFrequencyPhase (LeanRidgelet.affineTranslation b)
          xi =
        ((LeanRidgelet.affineTranslationCharacter xi) b)
    theorem LeanRidgelet.affineFrequencyPhase_translation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] (b xi : E) :
      LeanRidgelet.affineFrequencyPhase
          (LeanRidgelet.affineTranslation b)
          xi =
        ((LeanRidgelet.affineTranslationCharacter
              xi)
            b)
    On the translation subgroup, the Fourier-side phase is precisely the Mackey translation
    character at the current frequency. 
  • complete
    theorem LeanRidgelet.affineFrequencyPhase_cocycle.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g h : E ≃ᵃ[] E) (xi : E) :
      LeanRidgelet.affineFrequencyPhase (g * h) xi =
        LeanRidgelet.affineFrequencyPhase g xi *
          LeanRidgelet.affineFrequencyPhase h
            (LeanRidgelet.affineDualAction g⁻¹ xi)
    theorem LeanRidgelet.affineFrequencyPhase_cocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      (g h : E ≃ᵃ[] E) (xi : E) :
      LeanRidgelet.affineFrequencyPhase
          (g * h) xi =
        LeanRidgelet.affineFrequencyPhase g
            xi *
          LeanRidgelet.affineFrequencyPhase h
            (LeanRidgelet.affineDualAction g⁻¹
              xi)
    The affine frequency phase is a multiplier cocycle for inverse dual pullback.  This is the
    character twist that distinguishes the Mackey representation from the untwisted quasi-regular
    action on the homogeneous orbit. 
  • complete
    def LeanRidgelet.affineFrequencyPhaseMultiplier.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (g : E ≃ᵃ[] E) :
      (MeasureTheory.Lp  2 MeasureTheory.volume) ≃ₗᵢ[]
        (MeasureTheory.Lp  2 MeasureTheory.volume)
    def LeanRidgelet.affineFrequencyPhaseMultiplier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) :
      (MeasureTheory.Lp  2
            MeasureTheory.volume) ≃ₗᵢ[]
        (MeasureTheory.Lp  2
            MeasureTheory.volume)
    Implementation after :=
    :=
      unimodularMultiplierLinearIsometryEquiv (affineFrequencyPhase g)
        (affineFrequencyPhase_aestronglyMeasurable g) (affineFrequencyPhase_norm_one g)
    Multiplication by the affine frequency phase, bundled as a unitary `Lp` operator. 
  • complete
    def LeanRidgelet.affineFrequencyLinearIsometryEquiv.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (g : E ≃ᵃ[] E) :
      (MeasureTheory.Lp  2 MeasureTheory.volume) ≃ₗᵢ[]
        (MeasureTheory.Lp  2 MeasureTheory.volume)
    def LeanRidgelet.affineFrequencyLinearIsometryEquiv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) :
      (MeasureTheory.Lp  2
            MeasureTheory.volume) ≃ₗᵢ[]
        (MeasureTheory.Lp  2
            MeasureTheory.volume)
    Implementation after :=
    :=
      (Unitary.linearIsometryEquiv (affineDualPullbackLpUnitaryRepresentation (E := E) g)).trans
        (affineFrequencyPhaseMultiplier g)
    The explicit Fourier-side affine operator: dual pullback followed by multiplication by the
    translation character. 
  • complete
    theorem LeanRidgelet.affineFrequencyLinearIsometryEquiv_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) (f : (MeasureTheory.Lp  2 MeasureTheory.volume)) :
      ((LeanRidgelet.affineFrequencyLinearIsometryEquiv g)
              f) =ᵐ[MeasureTheory.volume]
        fun xi 
        LeanRidgelet.affineFrequencyPhase g xi *
          ((NNReal.sqrt LinearMap.det g.linear‖₊) *
            f (g.linear.adjoint xi))
    theorem LeanRidgelet.affineFrequencyLinearIsometryEquiv_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E)
      (f :
        (MeasureTheory.Lp  2
            MeasureTheory.volume)) :
      ((LeanRidgelet.affineFrequencyLinearIsometryEquiv
                g)
              f) =ᵐ[MeasureTheory.volume]
        fun xi 
        LeanRidgelet.affineFrequencyPhase g
            xi *
          ((NNReal.sqrt
                  LinearMap.det
                      g.linear‖₊) *
            f (g.linear.adjoint xi))
    The explicit Fourier-side affine operator acts by character multiplication and adjoint
    pullback on every `L²` class. 
  • complete
    theorem LeanRidgelet.affineFourierLpUnitaryRepresentation_schwartz_input_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) (f : SchwartzMap E ) :
      ((Unitary.linearIsometryEquiv
                (LeanRidgelet.affineFourierLpUnitaryRepresentation g))
              (f.toLp 2 MeasureTheory.volume)) =ᵐ[MeasureTheory.volume]
        fun xi 
        Real.fourierChar (-inner  (g 0) xi) 
          (NNReal.sqrt LinearMap.det g.linear‖₊) 
            f (g.linear.adjoint xi)
    theorem LeanRidgelet.affineFourierLpUnitaryRepresentation_schwartz_input_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) (f : SchwartzMap E ) :
      ((Unitary.linearIsometryEquiv
                (LeanRidgelet.affineFourierLpUnitaryRepresentation
                  g))
              (f.toLp 2
                MeasureTheory.volume)) =ᵐ[MeasureTheory.volume]
        fun xi 
        Real.fourierChar (-inner  (g 0) xi) 
          (NNReal.sqrt
                  LinearMap.det
                      g.linear‖₊) 
            f (g.linear.adjoint xi)
    The Plancherel-conjugated representation has the explicit affine frequency formula on the
    ordinary Schwartz core (rather than only on Fourier transforms of Schwartz vectors). 
  • complete
    theorem LeanRidgelet.affineFrequencyLinearIsometryEquiv_eq_fourierRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) :
      LeanRidgelet.affineFrequencyLinearIsometryEquiv g =
        Unitary.linearIsometryEquiv
          (LeanRidgelet.affineFourierLpUnitaryRepresentation g)
    theorem LeanRidgelet.affineFrequencyLinearIsometryEquiv_eq_fourierRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) :
      LeanRidgelet.affineFrequencyLinearIsometryEquiv
          g =
        Unitary.linearIsometryEquiv
          (LeanRidgelet.affineFourierLpUnitaryRepresentation
            g)
    The explicit frequency operator is exactly the Plancherel-conjugated affine action on all of
    `L²`.  The proof uses the explicit formulas on the dense Schwartz core and continuity of both
    unitary operators. 
  • complete
    theorem LeanRidgelet.affineFourierLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E) (f : (MeasureTheory.Lp  2 MeasureTheory.volume)) :
      ((Unitary.linearIsometryEquiv
                (LeanRidgelet.affineFourierLpUnitaryRepresentation g))
              f) =ᵐ[MeasureTheory.volume]
        fun xi 
        LeanRidgelet.affineFrequencyPhase g xi *
          ((NNReal.sqrt LinearMap.det g.linear‖₊) *
            f (g.linear.adjoint xi))
    theorem LeanRidgelet.affineFourierLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g : E ≃ᵃ[] E)
      (f :
        (MeasureTheory.Lp  2
            MeasureTheory.volume)) :
      ((Unitary.linearIsometryEquiv
                (LeanRidgelet.affineFourierLpUnitaryRepresentation
                  g))
              f) =ᵐ[MeasureTheory.volume]
        fun xi 
        LeanRidgelet.affineFrequencyPhase g
            xi *
          ((NNReal.sqrt
                  LinearMap.det
                      g.linear‖₊) *
            f (g.linear.adjoint xi))
    Consequently, the Plancherel-conjugated affine representation has the character-times-dual-
    pullback formula for every `L²` class. 
Theorem4.3.3
Statement uses 5
Statement dependency previews
Preview
Theorem 4.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Theorem 4.3.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Group, Fourier, and orbit input for Mackey induction. The affine group is realized as a locally compact topological semidirect product, and the determinant-corrected physical representation is strongly continuous. Plancherel conjugation gives an equivalent frequency representation with bounded intertwiners in both directions; the explicit dual-pullback and character model agrees with it on all of . The contragredient action has one conull nonzero orbit. At a chosen frequency, the translation group semidirect the little group is a closed locally compact inducing subgroup carrying a continuous irreducible character. The orbit map descends to an equivariant homeomorphism from its left-coset space to that orbit. Pullback to the orbit subtype is a surjective isometry, so physical, frequency, and intrinsic-orbit irreducibility are equivalent. The measure, section, and commutant layers are separated below. The full linear group is essential: positive dilations alone leave two frequency half-lines.

Lean code for Theorem4.3.318 declarations
  • def LeanRidgelet.affineTopologicalLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (mu : MeasureTheory.Measure E) [mu.IsAddHaarMeasure]
      [MeasureTheory.SigmaFinite mu] :
      UnitaryRepresentation (AffineEquiv.TopologicalSemidirectProduct E)
        (MeasureTheory.Lp  2 mu)
    def LeanRidgelet.affineTopologicalLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (mu : MeasureTheory.Measure E)
      [mu.IsAddHaarMeasure]
      [MeasureTheory.SigmaFinite mu] :
      UnitaryRepresentation
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        (MeasureTheory.Lp  2 mu)
    Implementation after :=
    :=
      (affineDataLpUnitaryRepresentation (Y := ℂ) mu).restrict
        (AffineEquiv.topologicalSemidirectProductEquiv E).toMonoidHom
    The affine data representation, reindexed by the locally compact semidirect-product model of
    the affine group.  This is the group model to which locally compact Mackey theory applies. 
  • complete
    theorem LeanRidgelet.affineTopologicalLpUnitaryRepresentation_isStronglyContinuous.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (mu : MeasureTheory.Measure E) [mu.IsAddHaarMeasure]
      [MeasureTheory.SigmaFinite mu] [mu.InnerRegularCompactLTTop]
      [MeasureTheory.IsLocallyFiniteMeasure mu] :
      (LeanRidgelet.affineTopologicalLpUnitaryRepresentation
          mu).IsStronglyContinuous
    theorem LeanRidgelet.affineTopologicalLpUnitaryRepresentation_isStronglyContinuous.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (mu : MeasureTheory.Measure E)
      [mu.IsAddHaarMeasure]
      [MeasureTheory.SigmaFinite mu]
      [mu.InnerRegularCompactLTTop]
      [MeasureTheory.IsLocallyFiniteMeasure
          mu] :
      (LeanRidgelet.affineTopologicalLpUnitaryRepresentation
          mu).IsStronglyContinuous
    The determinant-corrected affine `L²` representation is strongly continuous on the locally
    compact semidirect-product model of the affine group. 
  • complete
    def LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] :
      UnitaryRepresentation (AffineEquiv.TopologicalSemidirectProduct E)
        (MeasureTheory.Lp  2 MeasureTheory.volume)
    def LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      UnitaryRepresentation
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        (MeasureTheory.Lp  2
            MeasureTheory.volume)
    Implementation after :=
    :=
      (affineTopologicalLpUnitaryRepresentation (volume : Measure E)).conjugate
        (Lp.fourierTransformₗᵢ E ℂ)
    The Fourier-side affine representation indexed by the locally compact topological
    semidirect-product model. 
  • complete
    def LeanRidgelet.affinePlancherelIntertwiningMap.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).toContRepresentation
        LeanRidgelet.affineFourierLpUnitaryRepresentation.toContRepresentation
    def LeanRidgelet.affinePlancherelIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).toContRepresentation
        LeanRidgelet.affineFourierLpUnitaryRepresentation.toContRepresentation
    Implementation after :=
    := ℂ) (volume : Measure E)).toContRepresentation →ⁱL
          (affineFourierLpUnitaryRepresentation (E := E)).toContRepresentation :=
      UnitaryRepresentation.conjugateIntertwiningMap
        (affineDataLpUnitaryRepresentation (Y := ℂ) (volume : Measure E))
        (Lp.fourierTransformₗᵢ E ℂ)
    The Plancherel transform, bundled as a bounded intertwiner from the physical-space affine
    representation to its frequency-space conjugate. 
  • complete
    def LeanRidgelet.affinePlancherelInverseIntertwiningMap.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        LeanRidgelet.affineFourierLpUnitaryRepresentation.toContRepresentation
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).toContRepresentation
    def LeanRidgelet.affinePlancherelInverseIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        LeanRidgelet.affineFourierLpUnitaryRepresentation.toContRepresentation
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).toContRepresentation
    Implementation after :=
    := E)).toContRepresentation →ⁱL
          (affineDataLpUnitaryRepresentation (Y := ℂ)
            (volume : Measure E)).toContRepresentation :=
      UnitaryRepresentation.conjugateInverseIntertwiningMap
        (affineDataLpUnitaryRepresentation (Y := ℂ) (volume : Measure E))
        (Lp.fourierTransformₗᵢ E ℂ)
    The inverse Plancherel transform, bundled as the inverse bounded intertwiner. 
  • def LeanRidgelet.affineDualOrbit.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] : Set E
    def LeanRidgelet.affineDualOrbit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] :
      Set E
    Implementation after :=
    := {xi | xi ≠ 0}
    The unique nonzero orbit for the dual action of the full affine linear subgroup. 
  • complete
    theorem LeanRidgelet.affineDualOrbit_transitive.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi eta : E} (hxi : xi  LeanRidgelet.affineDualOrbit)
      (heta : eta  LeanRidgelet.affineDualOrbit) :
       L, L.symm.adjoint xi = eta
    theorem LeanRidgelet.affineDualOrbit_transitive.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi eta : E}
      (hxi :
        xi  LeanRidgelet.affineDualOrbit)
      (heta :
        eta  LeanRidgelet.affineDualOrbit) :
       L, L.symm.adjoint xi = eta
    The contragredient `GL(E)` action is transitive on the affine dual orbit. 
  • def LeanRidgelet.affineTopologicalMackeySubgroup.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (xi : E) : ClosedSubgroup (AffineEquiv.TopologicalSemidirectProduct E)
    def LeanRidgelet.affineTopologicalMackeySubgroup.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      ClosedSubgroup
        (AffineEquiv.TopologicalSemidirectProduct
          E)
    Implementation after :=
    := (affineTopologicalDualLittleGroup xi).comap SemidirectProduct.rightHom
      isClosed' := (affineTopologicalDualLittleGroup xi).isClosed'.preimage
        (SemidirectProduct.continuous_right
          (φ := AffineEquiv.continuousLinearMultiplicativeActionHom E))
    The Mackey inducing subgroup `E ⋊ G_xi` inside the topological affine group. It contains all
    translations and restricts the linear factor to the stabilizer of the frequency `xi`. 
  • def LeanRidgelet.affineTopologicalMackeyCharacter.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (xi : E) :
      (LeanRidgelet.affineTopologicalMackeySubgroup xi) →* Circle
    def LeanRidgelet.affineTopologicalMackeyCharacter.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      (LeanRidgelet.affineTopologicalMackeySubgroup
            xi) →*
        Circle
    Implementation after :=
    := affineTranslationCharacter xi p.1.left.toAdd
      map_one' := by simp
      map_mul' p q := by
        change affineTranslationCharacter xi
            (p.1.left.toAdd + (p.1.right : E →L[ℝ] E) q.1.left.toAdd) =
          affineTranslationCharacter xi p.1.left.toAdd *
            affineTranslationCharacter xi q.1.left.toAdd
        rw [(affineTranslationCharacter xi).map_add_eq_mul]
        congr 1
        exact affineTranslationCharacter_topological_linear_apply p.property q.1.left.toAdd
    The character of the inducing subgroup: it is the frequency character on translations and
    is trivial on the little group. 
  • def LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      UnitaryRepresentation
        (LeanRidgelet.affineTopologicalMackeySubgroup xi) 
    def LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      UnitaryRepresentation
        (LeanRidgelet.affineTopologicalMackeySubgroup
            xi)
        
    Implementation after :=
    :=
      UnitaryRepresentation.ofCircleCharacter (affineTopologicalMackeyCharacter xi)
    The one-dimensional unitary representation of the Mackey inducing subgroup. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      (LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation
          xi).IsTopologicallyIrreducible
    theorem LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      (LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation
          xi).IsTopologicallyIrreducible
    The Mackey inducing representation is irreducible because its Hilbert space is the complex
    line. 
  • def LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0) :
      AffineEquiv.TopologicalSemidirectProduct E 
          (LeanRidgelet.affineTopologicalMackeySubgroup xi) ≃ₜ
        LeanRidgelet.affineDualOrbit
    def LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0) :
      AffineEquiv.TopologicalSemidirectProduct
            E 
          (LeanRidgelet.affineTopologicalMackeySubgroup
              xi) ≃ₜ
        LeanRidgelet.affineDualOrbit
    Implementation after :=
    := E) :=
      (affineTopologicalMackeyQuotientEquivDualOrbit hxi).toHomeomorphOfContinuousOpen
        (continuous_affineTopologicalMackeyQuotientEquivDualOrbit hxi)
        (isOpenMap_affineTopologicalMackeyQuotientOrbitMap hxi)
    The homogeneous left-coset space is homeomorphic to the nonzero dual orbit. 
  • def LeanRidgelet.affineDualOrbitSubtypeMeasure.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      MeasureTheory.Measure LeanRidgelet.affineDualOrbit
    def LeanRidgelet.affineDualOrbitSubtypeMeasure.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      MeasureTheory.Measure
        LeanRidgelet.affineDualOrbit
    Implementation after :=
    := E)) :=
      Measure.comap Subtype.val (volume : Measure E)
    The intrinsic measure on the nonzero-frequency subtype, obtained by pulling Lebesgue measure
    back along the subtype inclusion. 
  • def LeanRidgelet.affineDualOrbitSubtypeLpEquiv.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] :
      (MeasureTheory.Lp  2 MeasureTheory.volume) ≃ₗᵢ[]
        (MeasureTheory.Lp  2 LeanRidgelet.affineDualOrbitSubtypeMeasure)
    def LeanRidgelet.affineDualOrbitSubtypeLpEquiv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E] :
      (MeasureTheory.Lp  2
            MeasureTheory.volume) ≃ₗᵢ[]
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)
    Implementation after :=
    := E)) :=
      LinearIsometryEquiv.ofSurjective (affineDualOrbitRestrictionLpLinearIsometry (E := E))
        affineDualOrbitRestrictionLpLinearIsometry_surjective
    The full frequency `L²` space and the intrinsic `L²` space on the nonzero-frequency subtype
    are canonically linearly isometric. 
  • complete
    def LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] :
      UnitaryRepresentation (AffineEquiv.TopologicalSemidirectProduct E)
        (MeasureTheory.Lp  2 LeanRidgelet.affineDualOrbitSubtypeMeasure)
    def LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E] :
      UnitaryRepresentation
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)
    Implementation after :=
    := E))) :=
      (affineTopologicalFourierLpUnitaryRepresentation (E := E)).conjugate
        (affineDualOrbitSubtypeLpEquiv (E := E))
    The explicit Fourier-side affine representation transported to the intrinsic `L²` space on
    the nonzero-frequency subtype. 
  • complete
    def LeanRidgelet.affineDualOrbitIntertwiningMap.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation.toContRepresentation
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
    def LeanRidgelet.affineDualOrbitIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation.toContRepresentation
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
    Implementation after :=
    := E)).toContRepresentation →ⁱL
          (affineTopologicalOrbitLpUnitaryRepresentation (E := E)).toContRepresentation :=
      UnitaryRepresentation.conjugateIntertwiningMap
        (affineTopologicalFourierLpUnitaryRepresentation (E := E))
        (affineDualOrbitSubtypeLpEquiv (E := E))
    The full frequency-space/orbit-space identification as a bounded intertwiner. 
  • complete
    def LeanRidgelet.affineDualOrbitInverseIntertwiningMap.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
        LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation.toContRepresentation
    def LeanRidgelet.affineDualOrbitInverseIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E] :
      ContIntertwiningMap
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
        LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation.toContRepresentation
    Implementation after :=
    := E)).toContRepresentation →ⁱL
          (affineTopologicalFourierLpUnitaryRepresentation (E := E)).toContRepresentation :=
      UnitaryRepresentation.conjugateInverseIntertwiningMap
        (affineTopologicalFourierLpUnitaryRepresentation (E := E))
        (affineDualOrbitSubtypeLpEquiv (E := E))
    The inverse orbit/full-frequency identification as a bounded intertwiner. 
  • complete
    theorem LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation_isTopologicallyIrreducible_iff.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] :
      LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.IsTopologicallyIrreducible 
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).IsTopologicallyIrreducible
    theorem LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation_isTopologicallyIrreducible_iff.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E] :
      LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.IsTopologicallyIrreducible 
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).IsTopologicallyIrreducible
    The orbit-measure, Fourier, and physical affine models are topologically irreducible
    simultaneously. 
Theorem4.3.4
uses 1used by 1L∃∀N

The homogeneous-space model. The quotient-orbit homeomorphism intertwines left translation on G/H with the affine dual action. The affine semidirect product is Polish and the closed subgroup quotient is second countable and Borel. Transporting the intrinsic orbit measure back through the homeomorphism gives a measure on the actual left-coset space; the homeomorphism and its inverse are measure preserving. Both transported measures are finite on compact sets, so compactly supported continuous sections belong to . Mathlib's composition API gives an onto linear isometry between orbit L^2 and homogeneous-space L^2, with inverse pullback supplying the surjectivity proof. Conjugation transports the explicit orbit representation to L^2(G/H) and bundles the equivalence and inverse as bounded intertwiners. Strong continuity and equivalence of irreducibility with the physical model follow without a measurable section. The normalized-section realization is constructed in the next node; only its spectral/commutant theorem remains afterward.

Lean code for Theorem4.3.421 declarations
  • complete
    theorem LeanRidgelet.instIsClosedAffineTopologicalMackeySubgroup.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      IsClosed (LeanRidgelet.affineTopologicalMackeySubgroup xi)
    theorem LeanRidgelet.instIsClosedAffineTopologicalMackeySubgroup.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      IsClosed
        (LeanRidgelet.affineTopologicalMackeySubgroup
              xi)
    The underlying subgroup of the closed Mackey inducing subgroup is closed.  This instance lets
    Mathlib equip its homogeneous coset space with the separated quotient topology. 
  • complete
    theorem LeanRidgelet.instSecondCountableTopologyAffineTopologicalMackeyQuotient.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      SecondCountableTopology
        (AffineEquiv.TopologicalSemidirectProduct E 
          (LeanRidgelet.affineTopologicalMackeySubgroup xi))
    theorem LeanRidgelet.instSecondCountableTopologyAffineTopologicalMackeyQuotient.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      SecondCountableTopology
        (AffineEquiv.TopologicalSemidirectProduct
            E 
          (LeanRidgelet.affineTopologicalMackeySubgroup
              xi))
    The homogeneous coset space of the affine group is second countable.  Recording the direct
    quotient instance avoids making downstream Borel-space synthesis rediscover second countability of
    the general linear factor. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q :
        AffineEquiv.TopologicalSemidirectProduct E 
          (LeanRidgelet.affineTopologicalMackeySubgroup xi)) :
      (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit hxi)
          (g  q) =
        g 
          (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi)
            q
    theorem LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        AffineEquiv.TopologicalSemidirectProduct
            E 
          (LeanRidgelet.affineTopologicalMackeySubgroup
              xi)) :
      (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
            hxi)
          (g  q) =
        g 
          (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi)
            q
    The quotient-orbit homeomorphism intertwines left translation on the homogeneous space with
    the affine dual action on the nonzero orbit. 
  • complete
    abbrev LeanRidgelet.AffineTopologicalMackeyQuotient.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (xi : E) : Type u_1
    abbrev LeanRidgelet.AffineTopologicalMackeyQuotient.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E) :
      Type u_1
    Implementation after :=
    :=
      AffineEquiv.TopologicalSemidirectProduct E ⧸
        (affineTopologicalMackeySubgroup xi).toSubgroup
    The homogeneous left-coset space of the full affine group by the Mackey inducing subgroup at
    the frequency `xi`. 
  • def LeanRidgelet.affineTopologicalMackeyQuotientMeasure.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0) :
      MeasureTheory.Measure
        (LeanRidgelet.AffineTopologicalMackeyQuotient xi)
    def LeanRidgelet.affineTopologicalMackeyQuotientMeasure.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      MeasureTheory.Measure
        (LeanRidgelet.AffineTopologicalMackeyQuotient
          xi)
    Implementation after :=
    :=
      (affineDualOrbitSubtypeMeasure (E := E)).map
        (affineTopologicalMackeyQuotientHomeomorphDualOrbit hxi).symm
    The measure on the affine homogeneous space obtained by transporting the intrinsic Lebesgue
    measure of the nonzero dual orbit through the quotient-orbit homeomorphism. 
  • complete
    theorem LeanRidgelet.instIsFiniteMeasureOnCompactsAffineDualOrbitSubtypeMeasure.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] :
      MeasureTheory.IsFiniteMeasureOnCompacts
        LeanRidgelet.affineDualOrbitSubtypeMeasure
    theorem LeanRidgelet.instIsFiniteMeasureOnCompactsAffineDualOrbitSubtypeMeasure.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      MeasureTheory.IsFiniteMeasureOnCompacts
        LeanRidgelet.affineDualOrbitSubtypeMeasure
    The intrinsic orbit measure is finite on compact sets.  This is the measure-theoretic input
    needed to send compactly supported continuous orbit sections to `L²`. 
  • complete
    theorem LeanRidgelet.instIsFiniteMeasureOnCompactsAffineTopologicalMackeyQuotientMeasure.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) :
      MeasureTheory.IsFiniteMeasureOnCompacts
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)
    theorem LeanRidgelet.instIsFiniteMeasureOnCompactsAffineTopologicalMackeyQuotientMeasure.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      MeasureTheory.IsFiniteMeasureOnCompacts
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi)
    The transported homogeneous-space measure is finite on compact sets. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotient_measurePreserving.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) :
      MeasureTheory.MeasurePreserving
        (⇑(LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
            hxi))
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)
        LeanRidgelet.affineDualOrbitSubtypeMeasure
    theorem LeanRidgelet.affineTopologicalMackeyQuotient_measurePreserving.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      MeasureTheory.MeasurePreserving
        (⇑(LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
            hxi))
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi)
        LeanRidgelet.affineDualOrbitSubtypeMeasure
    The quotient-orbit homeomorphism preserves the transported homogeneous-space measure. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotient_symm_measurePreserving.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) :
      MeasureTheory.MeasurePreserving
        (⇑(LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi).symm)
        LeanRidgelet.affineDualOrbitSubtypeMeasure
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)
    theorem LeanRidgelet.affineTopologicalMackeyQuotient_symm_measurePreserving.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      MeasureTheory.MeasurePreserving
        (⇑(LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi).symm)
        LeanRidgelet.affineDualOrbitSubtypeMeasure
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi)
    The inverse quotient-orbit homeomorphism is also measure preserving. 
  • complete
    def LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) :
      (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure) →ₗᵢ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure) →ₗᵢ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    := E)) →ₗᵢ[ℂ]
          Lp ℂ 2 (affineTopologicalMackeyQuotientMeasure hxi) :=
      Lp.compMeasurePreservingₗᵢ ℂ
        (affineTopologicalMackeyQuotientHomeomorphDualOrbit hxi)
        (affineTopologicalMackeyQuotient_measurePreserving hxi)
    Pullback through the quotient-orbit homeomorphism as a linear isometry from orbit `L²` to
    homogeneous-space `L²`. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      ((LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry hxi)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        f 
          (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi)
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      ((LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry
                hxi)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        f 
          (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi)
    The homogeneous-space pullback is represented almost everywhere by composition with the
    quotient-orbit homeomorphism. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry_surjective.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) :
      Function.Surjective
        (LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry hxi)
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry_surjective.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      Function.Surjective
        (LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry
            hxi)
    Pullback through the quotient-orbit homeomorphism is onto; its inverse is pullback through the
    inverse homeomorphism. 
  • complete
    def LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0) :
      (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure) ≃ₗᵢ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure) ≃ₗᵢ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    := E)) ≃ₗᵢ[ℂ]
          Lp ℂ 2 (affineTopologicalMackeyQuotientMeasure hxi) :=
      LinearIsometryEquiv.ofSurjective
        (affineTopologicalMackeyQuotientLpLinearIsometry hxi)
        (affineTopologicalMackeyQuotientLpLinearIsometry_surjective hxi)
    The intrinsic orbit `L²` space and the homogeneous quotient `L²` space are canonically
    linearly isometric. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      (LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv hxi) f =
        (LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry hxi) f
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      (LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv
            hxi)
          f =
        (LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry
            hxi)
          f
  • complete
    def LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      UnitaryRepresentation (AffineEquiv.TopologicalSemidirectProduct E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      UnitaryRepresentation
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    :=
      (affineTopologicalOrbitLpUnitaryRepresentation (E := E)).conjugate
        (affineTopologicalMackeyQuotientLpEquiv hxi)
    The explicit affine representation in its homogeneous-space `L²(G/H)` model.  It is
    transported through the quotient-orbit homeomorphism, so no representative or measurable section
    of `G/H` is chosen. 
  • complete
    def LeanRidgelet.affineTopologicalMackeyQuotientIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      ContIntertwiningMap
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
        (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
            hxi).toContRepresentation
    def LeanRidgelet.affineTopologicalMackeyQuotientIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      ContIntertwiningMap
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
        (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
            hxi).toContRepresentation
    Implementation after :=
    := E)).toContRepresentation →ⁱL
          (affineTopologicalMackeyQuotientLpUnitaryRepresentation hxi).toContRepresentation :=
      UnitaryRepresentation.conjugateIntertwiningMap
        (affineTopologicalOrbitLpUnitaryRepresentation (E := E))
        (affineTopologicalMackeyQuotientLpEquiv hxi)
    The orbit/homogeneous-space identification as a bounded intertwiner. 
  • complete
    def LeanRidgelet.affineTopologicalMackeyQuotientInverseIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      ContIntertwiningMap
        (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
            hxi).toContRepresentation
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
    def LeanRidgelet.affineTopologicalMackeyQuotientInverseIntertwiningMap.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      ContIntertwiningMap
        (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
            hxi).toContRepresentation
        LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation.toContRepresentation
    Implementation after :=
    := E)).toContRepresentation :=
      UnitaryRepresentation.conjugateInverseIntertwiningMap
        (affineTopologicalOrbitLpUnitaryRepresentation (E := E))
        (affineTopologicalMackeyQuotientLpEquiv hxi)
    The inverse homogeneous-space/orbit identification as a bounded intertwiner. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientIntertwiningMap_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      (LeanRidgelet.affineTopologicalMackeyQuotientIntertwiningMap hxi) f =
        (LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv hxi) f
    theorem LeanRidgelet.affineTopologicalMackeyQuotientIntertwiningMap_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      (LeanRidgelet.affineTopologicalMackeyQuotientIntertwiningMap
            hxi)
          f =
        (LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv
            hxi)
          f
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientInverseIntertwiningMap_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (LeanRidgelet.affineTopologicalMackeyQuotientInverseIntertwiningMap
            hxi)
          f =
        (LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv hxi).symm f
    theorem LeanRidgelet.affineTopologicalMackeyQuotientInverseIntertwiningMap_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (LeanRidgelet.affineTopologicalMackeyQuotientInverseIntertwiningMap
            hxi)
          f =
        (LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv
              hxi).symm
          f
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_isStronglyContinuous.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
          hxi).IsStronglyContinuous
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_isStronglyContinuous.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
          hxi).IsStronglyContinuous
    The homogeneous-space representation is strongly continuous. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_isTopologicallyIrreducible_iff.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
            hxi).IsTopologicallyIrreducible 
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).IsTopologicallyIrreducible
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_isTopologicallyIrreducible_iff.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
            hxi).IsTopologicallyIrreducible 
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).IsTopologicallyIrreducible
    The homogeneous-space, orbit, Fourier, and physical affine models are topologically
    irreducible simultaneously. 
Definition4.3.5
Statement uses 2
Statement dependency previews
Preview
Definition 4.2.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

Quasi-invariance and the character twist. Injectivity of measure pushforward through the measurable orbit inclusion first transfers the ambient determinant formula to the intrinsic orbit. Equivariance of the quotient-orbit homeomorphism then gives the quotient formula both as a constant scalar multiple and as withDensity. The general quasi-invariant construction produces the untwisted quasi-regular unitary representation, whose representative is |\det L|^{1/2} f(g^{-1}q). The separately defined character phase is continuous, pointwise unimodular, satisfies the multiplier cocycle law, and restricts on translations to the frequency character. The general twisting construction bundles their product and proves its explicit a.e. action formula. The inverse transport equivalences are also identified a.e.; quasi-measure- preserving composition then proves equality with the independently transported Fourier model.

Lean code for Definition4.3.529 declarations
  • def LeanRidgelet.affineTopologicalDualJacobian.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g : AffineEquiv.TopologicalSemidirectProduct E) : NNReal
    def LeanRidgelet.affineTopologicalDualJacobian.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      NNReal
    Implementation after :=
    :=
      affineDualJacobian (AffineEquiv.topologicalSemidirectProductEquiv E g) 0
    The constant Radon--Nikodym density of the inverse dual action, written in the topological
    semidirect-product coordinates used by Mackey theory. 
  • complete
    theorem LeanRidgelet.affineTopologicalDualJacobian_eq_inv.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineTopologicalDualJacobian g =
        (LeanRidgelet.affineTopologicalJacobian g)⁻¹
    theorem LeanRidgelet.affineTopologicalDualJacobian_eq_inv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineTopologicalDualJacobian
          g =
        (LeanRidgelet.affineTopologicalJacobian
            g)⁻¹
    The dual density is the inverse of the data-side affine density. 
  • complete
    theorem LeanRidgelet.measurable_affineTopologicalDualOrbit_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      Measurable fun eta  g  eta
    theorem LeanRidgelet.measurable_affineTopologicalDualOrbit_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      Measurable fun eta  g  eta
    Each affine group element acts measurably on the intrinsic nonzero dual orbit. 
  • complete
    theorem LeanRidgelet.affineDualOrbitSubtypeMeasure_map_inv_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] (g : AffineEquiv.TopologicalSemidirectProduct E) :
      MeasureTheory.Measure.map (fun eta  g⁻¹  eta)
          LeanRidgelet.affineDualOrbitSubtypeMeasure =
        (LeanRidgelet.affineTopologicalDualJacobian g) 
          LeanRidgelet.affineDualOrbitSubtypeMeasure
    theorem LeanRidgelet.affineDualOrbitSubtypeMeasure_map_inv_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      MeasureTheory.Measure.map
          (fun eta  g⁻¹  eta)
          LeanRidgelet.affineDualOrbitSubtypeMeasure =
        (LeanRidgelet.affineTopologicalDualJacobian
              g) 
          LeanRidgelet.affineDualOrbitSubtypeMeasure
    The intrinsic orbit measure is strongly quasi-invariant under the dual affine action, with
    the same constant density as ambient Lebesgue measure. 
  • complete
    theorem LeanRidgelet.affineDualOrbitSubtype_quasiMeasurePreserving.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] (g : AffineEquiv.TopologicalSemidirectProduct E) :
      MeasureTheory.Measure.QuasiMeasurePreserving (fun eta  g⁻¹  eta)
        LeanRidgelet.affineDualOrbitSubtypeMeasure
        LeanRidgelet.affineDualOrbitSubtypeMeasure
    theorem LeanRidgelet.affineDualOrbitSubtype_quasiMeasurePreserving.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      MeasureTheory.Measure.QuasiMeasurePreserving
        (fun eta  g⁻¹  eta)
        LeanRidgelet.affineDualOrbitSubtypeMeasure
        LeanRidgelet.affineDualOrbitSubtypeMeasure
    Inverse dual translation is quasi-measure-preserving on the intrinsic nonzero orbit. 
  • def LeanRidgelet.affineTopologicalMackeyQuotientJacobian.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.AffineTopologicalMackeyQuotient xi  NNReal
    def LeanRidgelet.affineTopologicalMackeyQuotientJacobian.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.AffineTopologicalMackeyQuotient
          xi 
        NNReal
    Implementation after :=
    :=
      affineTopologicalDualJacobian g
    The Radon--Nikodym cocycle for the transported measure on the affine homogeneous space.  It
    is constant on the quotient because the dual action has constant determinant density. 
  • complete
    theorem LeanRidgelet.measurable_affineTopologicalMackeyQuotient_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      Measurable fun q  g  q
    theorem LeanRidgelet.measurable_affineTopologicalMackeyQuotient_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      Measurable fun q  g  q
    Left translation on the affine homogeneous quotient is measurable. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientMeasure_map_inv_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      MeasureTheory.Measure.map (fun q  g⁻¹  q)
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi) =
        (LeanRidgelet.affineTopologicalDualJacobian g) 
          LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi
    theorem LeanRidgelet.affineTopologicalMackeyQuotientMeasure_map_inv_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      MeasureTheory.Measure.map
          (fun q  g⁻¹  q)
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi) =
        (LeanRidgelet.affineTopologicalDualJacobian
              g) 
          LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi
    The quotient-orbit homeomorphism transports the constant-density quasi-invariance of the
    intrinsic orbit measure to the homogeneous space. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_measurable.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      Measurable (LeanRidgelet.affineTopologicalMackeyQuotientJacobian g)
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_measurable.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      Measurable
        (LeanRidgelet.affineTopologicalMackeyQuotientJacobian
          g)
    The homogeneous-space Jacobian is measurable. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientJacobian g q  0
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientJacobian
          g q 
        0
    The homogeneous-space Jacobian is everywhere nonzero. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientJacobian 1 q = 1
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientJacobian
          1 q =
        1
    The homogeneous-space Jacobian at the identity is one. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_cocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g h : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientJacobian (g * h) q =
        LeanRidgelet.affineTopologicalMackeyQuotientJacobian g (h  q) *
          LeanRidgelet.affineTopologicalMackeyQuotientJacobian h q
    theorem LeanRidgelet.affineTopologicalMackeyQuotientJacobian_cocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g h :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientJacobian
          (g * h) q =
        LeanRidgelet.affineTopologicalMackeyQuotientJacobian
            g (h  q) *
          LeanRidgelet.affineTopologicalMackeyQuotientJacobian
            h q
    The homogeneous-space density satisfies the Radon--Nikodym cocycle law. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientMeasure_map_eq_withDensity.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      MeasureTheory.Measure.map (fun q  g⁻¹  q)
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi) =
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi).withDensity
          fun q 
          (LeanRidgelet.affineTopologicalMackeyQuotientJacobian g q)
    theorem LeanRidgelet.affineTopologicalMackeyQuotientMeasure_map_eq_withDensity.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      MeasureTheory.Measure.map
          (fun q  g⁻¹  q)
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi) =
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi).withDensity
          fun q 
          (LeanRidgelet.affineTopologicalMackeyQuotientJacobian
              g q)
    Strong quasi-invariance of the homogeneous-space measure, in the `withDensity` form consumed
    by the general quasi-invariant `L²` construction. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientRadonNikodymWeight.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineTopologicalMackeyQuotientJacobian g q =
        (NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g))
    theorem LeanRidgelet.affineTopologicalMackeyQuotientRadonNikodymWeight.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineTopologicalMackeyQuotientJacobian
          g q =
        (NNReal.sqrt
              (LeanRidgelet.affineTopologicalJacobian
                g))
    Folland's Radon--Nikodym correction on the homogeneous quotient is the positive square root
    of the data-side affine determinant. 
  • def LeanRidgelet.affineTopologicalMackeyQuotientPhase.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) : 
    def LeanRidgelet.affineTopologicalMackeyQuotientPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      
    Implementation after :=
    :=
      affineFrequencyPhase (AffineEquiv.topologicalSemidirectProductEquiv E g)
        (affineTopologicalMackeyQuotientHomeomorphDualOrbit hxi q).1
    The Mackey character phase on the affine homogeneous quotient, obtained from the frequency
    attached to a coset by the quotient-orbit homeomorphism. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientPhase_cocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g h : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi (g * h) q =
        LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi g q *
          LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi h (g⁻¹  q)
    theorem LeanRidgelet.affineTopologicalMackeyQuotientPhase_cocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g h :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientPhase
          hxi (g * h) q =
        LeanRidgelet.affineTopologicalMackeyQuotientPhase
            hxi g q *
          LeanRidgelet.affineTopologicalMackeyQuotientPhase
            hxi h (g⁻¹  q)
    The quotient phase is a multiplier cocycle for inverse left translation. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientPhase_norm_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi g q = 1
    theorem LeanRidgelet.affineTopologicalMackeyQuotientPhase_norm_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientPhase
            hxi g q =
        1
    The Mackey character phase is pointwise unimodular. 
  • complete
    theorem LeanRidgelet.continuous_affineTopologicalMackeyQuotientPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      Continuous (LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi g)
    theorem LeanRidgelet.continuous_affineTopologicalMackeyQuotientPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      Continuous
        (LeanRidgelet.affineTopologicalMackeyQuotientPhase
          hxi g)
    The Mackey character phase is continuous in the homogeneous-space variable. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientPhase_translation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0) (b : E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi
          ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
            (LeanRidgelet.affineTranslation b))
          q =
        ((LeanRidgelet.affineTranslationCharacter
              ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                    hxi)
                  q))
            b)
    theorem LeanRidgelet.affineTopologicalMackeyQuotientPhase_translation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0) (b : E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeyQuotientPhase
          hxi
          ((AffineEquiv.topologicalSemidirectProductEquiv
                E).symm
            (LeanRidgelet.affineTranslation
              b))
          q =
        ((LeanRidgelet.affineTranslationCharacter
              ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                    hxi)
                  q))
            b)
    On translations, the quotient phase is exactly the Mackey translation character at the
    frequency represented by the coset. 
  • def LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      UnitaryRepresentation (AffineEquiv.TopologicalSemidirectProduct E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      UnitaryRepresentation
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    :=
      quasiInvariantLpUnitaryRepresentation
        (affineTopologicalMackeyQuotientJacobian (xi := xi))
        measurable_affineTopologicalMackeyQuotient_smul
        (affineTopologicalMackeyQuotientMeasure_map_eq_withDensity hxi)
        affineTopologicalMackeyQuotientJacobian_measurable
        affineTopologicalMackeyQuotientJacobian_ne_zero
        affineTopologicalMackeyQuotientJacobian_one
        affineTopologicalMackeyQuotientJacobian_cocycle
    The untwisted quasi-regular unitary representation on the affine homogeneous quotient.  This
    is the measure-theoretic base of the Mackey model; the inducing character supplies an additional
    unit-modulus phase in the representation transported from the frequency orbit below. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight
            LeanRidgelet.affineTopologicalMackeyQuotientJacobian)
          g fun q  f q
    theorem LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight
            LeanRidgelet.affineTopologicalMackeyQuotientJacobian)
          g fun q  f q
    The quotient quasi-regular representation has Folland's determinant-corrected pullback as an
    almost-everywhere representative. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation_apply_ae_explicit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        fun q 
        (NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g)) 
          f (g⁻¹  q)
    theorem LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation_apply_ae_explicit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        fun q 
        (NNReal.sqrt
                (LeanRidgelet.affineTopologicalJacobian
                  g)) 
          f (g⁻¹  q)
    Explicitly, the quotient quasi-regular action is pullback by inverse left translation times
    the square root of the affine determinant. 
  • def LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      UnitaryRepresentation (AffineEquiv.TopologicalSemidirectProduct E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      UnitaryRepresentation
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    :=
      twistedQuasiInvariantLpUnitaryRepresentation
        (affineTopologicalMackeyQuotientJacobian (xi := xi))
        measurable_affineTopologicalMackeyQuotient_smul
        (affineTopologicalMackeyQuotientMeasure_map_eq_withDensity hxi)
        affineTopologicalMackeyQuotientJacobian_measurable
        affineTopologicalMackeyQuotientJacobian_ne_zero
        affineTopologicalMackeyQuotientJacobian_one
        affineTopologicalMackeyQuotientJacobian_cocycle
        (affineTopologicalMackeyQuotientPhase hxi)
        (fun g ↦ (continuous_affineTopologicalMackeyQuotientPhase hxi g).aestronglyMeasurable)
        (fun g ↦ Filter.Eventually.of_forall
          (affineTopologicalMackeyQuotientPhase_norm_one hxi g))
        (affineTopologicalMackeyQuotientPhase_one hxi)
        (affineTopologicalMackeyQuotientPhase_cocycle hxi)
    The character-twisted quasi-regular representation on `L²(G/H)`.  Its two factors are
    constructed independently: the quotient measure supplies the Radon--Nikodym correction, while
    the Mackey translation character supplies the unimodular multiplier cocycle. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation_apply_ae_explicit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        fun q 
        LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi g q *
          ((NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g)) *
            f (g⁻¹  q))
    theorem LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation_apply_ae_explicit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        fun q 
        LeanRidgelet.affineTopologicalMackeyQuotientPhase
            hxi g q *
          ((NNReal.sqrt
                  (LeanRidgelet.affineTopologicalJacobian
                    g)) *
            f (g⁻¹  q))
    The character-twisted quotient representation acts by the Mackey phase times the positive
    square root of the affine determinant and inverse left translation. 
  • complete
    theorem LeanRidgelet.affineDualOrbitSubtypeLpEquiv_symm_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E]
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      (fun eta 
          (LeanRidgelet.affineDualOrbitSubtypeLpEquiv.symm f)
            eta) =ᵐ[LeanRidgelet.affineDualOrbitSubtypeMeasure]
        f
    theorem LeanRidgelet.affineDualOrbitSubtypeLpEquiv_symm_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      (fun eta 
          (LeanRidgelet.affineDualOrbitSubtypeLpEquiv.symm
                  f)
            eta) =ᵐ[LeanRidgelet.affineDualOrbitSubtypeMeasure]
        f
    The inverse intrinsic-orbit equivalence agrees almost everywhere with the original full-space
    class on the conull nonzero subtype. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv_symm_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      ((LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv hxi).symm
              f) =ᵐ[LeanRidgelet.affineDualOrbitSubtypeMeasure]
        f 
          (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                hxi).symm
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv_symm_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      ((LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv
                  hxi).symm
              f) =ᵐ[LeanRidgelet.affineDualOrbitSubtypeMeasure]
        f 
          (LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                hxi).symm
    The inverse homogeneous-space equivalence is represented by pullback through the inverse
    quotient-orbit homeomorphism. 
  • complete
    theorem LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] (g : AffineEquiv.TopologicalSemidirectProduct E)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      ((LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation g)
              f) =ᵐ[LeanRidgelet.affineDualOrbitSubtypeMeasure]
        fun eta 
        LeanRidgelet.affineFrequencyPhase
            ((AffineEquiv.topologicalSemidirectProductEquiv E) g) eta *
          ((NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g)) *
            f (g⁻¹  eta))
    theorem LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (f :
        (MeasureTheory.Lp  2
            LeanRidgelet.affineDualOrbitSubtypeMeasure)) :
      ((LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation
                  g)
              f) =ᵐ[LeanRidgelet.affineDualOrbitSubtypeMeasure]
        fun eta 
        LeanRidgelet.affineFrequencyPhase
            ((AffineEquiv.topologicalSemidirectProductEquiv
                E)
              g)
            eta *
          ((NNReal.sqrt
                  (LeanRidgelet.affineTopologicalJacobian
                    g)) *
            f (g⁻¹  eta))
    The transported intrinsic-orbit representation retains the explicit
    character-times-determinant-corrected dual pullback formula. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        fun q 
        LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi g q *
          ((NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g)) *
            f (g⁻¹  q))
    theorem LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (((LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        fun q 
        LeanRidgelet.affineTopologicalMackeyQuotientPhase
            hxi g q *
          ((NNReal.sqrt
                  (LeanRidgelet.affineTopologicalJacobian
                    g)) *
            f (g⁻¹  q))
    The independently transported homogeneous-space representation has the same explicit action
    as the character-twisted quasi-regular construction. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation_eq_transported.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation
          hxi =
        LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
          hxi
    theorem LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation_eq_transported.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation
          hxi =
        LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
          hxi
    The character-twisted quasi-regular representation is exactly the homogeneous-space model
    obtained independently by transporting the explicit Fourier representation. 
Theorem4.3.6
Statement uses 8
Statement dependency previews
Preview
Definition 4.3.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

Normalized-section unitary induction. Since the inducing subgroup contains every translation, the choice-based quotient representative can be normalized by discarding its translation coordinate without changing its coset. This gives a right inverse s:G/H\to G and hence the reentry cocycle s(q)^{-1}g s(g^{-1}q) in the inducing subgroup. Applying the inducing character to this cocycle is proved, by the adjoint identity for the linear coordinate of s(q), to equal the independently constructed Fourier phase. The resulting quasi-invariant representation is therefore exactly both the character-twisted quotient model and the transported Fourier model; it is strongly continuous, and its irreducibility is equivalent to Theorem 2.5. No measurability of the raw choice function is assumed: regularity is obtained from the proved phase equality. Measurable-set indicator operators form its canonical projection family and satisfy P_s\pi(g)=\pi(g)P_{g^{-1}s}. Pure translations fix the quotient and have unit Jacobian, so their restriction is proved a.e. to be multiplication by the orbit-frequency character. The quotient coordinate is a measurable embedding into frequency space, and the translation restriction is identified with the general bundled Fourier-character multiplier. The derived affine Theorem-4.44 step is source-level complete: finite-character density in L^2 of an arbitrary finite measure is proved in the Mathlib candidate layer by characteristic-function uniqueness. The spectral-subspace and self-adjoint-decomposition remainder of Theorem 6.28 is proved as well. Compactly supported continuous scalar sections are bundled into ; their identity-coset values define the extracted closed inducing fiber. Haar-integrated smoothing is defined for this affine representation. A sequence of nonnegative compactly supported Haar probability kernels is constructed with supports shrinking to the identity; the smoothed vectors stay in the invariant closed subspace and converge in to the input. The compact-kernel group-convolution formula is now proved continuous in the Mathlib candidate layer by reduction to additive convolution on the opposite group. Once a smoothed vector has a continuous quotient representative, the general compact-multiplier API keeps its Urysohn cutoffs in the same subspace, and a diagonal sequence proves regular-section density. The general theorem identifying a Bochner integral in scalar with a family of pointwise representatives integrable over the finite-measure slices is also proved, and applying it to the measurable induced-model lift finishes Lemma 6.29: the smoothed vector agrees almost everywhere with the pointwise convolution, which is continuous. Indicator and representation stability, as well as the classification of closed complex subspaces of the one-dimensional fiber, are proved. The extreme-subspace part of Lemma 6.30 is now proved as well.

Lean code for Theorem4.3.659 declarations
  • def LeanRidgelet.affineTopologicalMackeySection.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      AffineEquiv.TopologicalSemidirectProduct E
    def LeanRidgelet.affineTopologicalMackeySection.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      AffineEquiv.TopologicalSemidirectProduct
        E
    Implementation after :=
    :=
      SemidirectProduct.inr (Quotient.out q).right
    A normalized set-theoretic section of the affine homogeneous quotient.  Starting from
    `Quotient.out`, it discards the translation coordinate.  This does not change the coset because
    the Mackey subgroup contains every translation, and it is the normalization for which the
    section-cocycle character agrees exactly with the Fourier phase. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySection_rightInverse.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} :
      Function.RightInverse LeanRidgelet.affineTopologicalMackeySection
        QuotientGroup.mk
    theorem LeanRidgelet.affineTopologicalMackeySection_rightInverse.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} :
      Function.RightInverse
        LeanRidgelet.affineTopologicalMackeySection
        QuotientGroup.mk
    The normalized affine section is a right inverse of the quotient map. 
  • def LeanRidgelet.affineTopologicalMackeySectionCocycle.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      (LeanRidgelet.affineTopologicalMackeySubgroup xi)
    def LeanRidgelet.affineTopologicalMackeySectionCocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      (LeanRidgelet.affineTopologicalMackeySubgroup
          xi)
    Implementation after :=
    :=
      QuotientGroup.leftCosetSectionCocycleOf
        (affineTopologicalMackeySubgroup xi).toSubgroup
        (affineTopologicalMackeySection (E := E))
        affineTopologicalMackeySection_rightInverse g q
    The Mackey-subgroup-valued reentry cocycle of the normalized affine section. 
  • def LeanRidgelet.affineTopologicalMackeySectionPhase.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) : 
    def LeanRidgelet.affineTopologicalMackeySectionPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      
    Implementation after :=
    :=
      (affineTopologicalMackeyCharacter xi
        (affineTopologicalMackeySectionCocycle g q) : Circle)
    Applying the inducing character to the normalized section cocycle gives the section-model
    phase. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit_eq_out.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi)
            q) =
        LeanRidgelet.affineTopologicalDualAction (Quotient.out q).right xi
    theorem LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit_eq_out.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
              hxi)
            q) =
        LeanRidgelet.affineTopologicalDualAction
          (Quotient.out q).right xi
    Evaluating the quotient-orbit homeomorphism through `Quotient.out` uses only the linear
    coordinate of the representative. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_eq_quotientPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase g q =
        LeanRidgelet.affineTopologicalMackeyQuotientPhase hxi g q
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_eq_quotientPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase
          g q =
        LeanRidgelet.affineTopologicalMackeyQuotientPhase
          hxi g q
    The phase obtained from the normalized section cocycle is exactly the explicit Fourier phase.
    Thus the homogeneous quotient representation already is the equivariant-section realization of
    unitary induction from `affineTopologicalMackeyCharacter`; no additional gauge multiplier is
    needed. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_cocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g h : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase (g * h) q =
        LeanRidgelet.affineTopologicalMackeySectionPhase g q *
          LeanRidgelet.affineTopologicalMackeySectionPhase h (g⁻¹  q)
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_cocycle.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g h :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase
          (g * h) q =
        LeanRidgelet.affineTopologicalMackeySectionPhase
            g q *
          LeanRidgelet.affineTopologicalMackeySectionPhase
            h (g⁻¹  q)
    The normalized section phase is a multiplier cocycle, as follows either from the general
    section-cocycle law or from its identification with the Fourier phase. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase 1 q = 1
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase
          1 q =
        1
    The normalized section phase is one at the identity. 
  • complete
    theorem LeanRidgelet.continuous_affineTopologicalMackeySectionPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      Continuous (LeanRidgelet.affineTopologicalMackeySectionPhase g)
    theorem LeanRidgelet.continuous_affineTopologicalMackeySectionPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      Continuous
        (LeanRidgelet.affineTopologicalMackeySectionPhase
          g)
    Although the chosen normalized section itself is only set-theoretic, its character phase is
    continuous: the explicit equality with the Fourier phase supplies the regularity. 
  • complete
    theorem LeanRidgelet.continuous_uncurry_affineTopologicalMackeySectionPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0) :
      Continuous
        (Function.uncurry LeanRidgelet.affineTopologicalMackeySectionPhase)
    theorem LeanRidgelet.continuous_uncurry_affineTopologicalMackeySectionPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0) :
      Continuous
        (Function.uncurry
          LeanRidgelet.affineTopologicalMackeySectionPhase)
    The normalized section phase is jointly continuous.  Rewriting it as the explicit Fourier phase
    separates the translation coordinate of the group element from the frequency attached to the coset,
    and both depend continuously on the pair. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_norm_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase g q = 1
    theorem LeanRidgelet.affineTopologicalMackeySectionPhase_norm_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      LeanRidgelet.affineTopologicalMackeySectionPhase
            g q =
        1
    The normalized section phase is pointwise unimodular. 
  • def LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      UnitaryRepresentation (AffineEquiv.TopologicalSemidirectProduct E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      UnitaryRepresentation
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    :=
      twistedQuasiInvariantLpUnitaryRepresentation
        (affineTopologicalMackeyQuotientJacobian (xi := xi))
        measurable_affineTopologicalMackeyQuotient_smul
        (affineTopologicalMackeyQuotientMeasure_map_eq_withDensity hxi)
        affineTopologicalMackeyQuotientJacobian_measurable
        affineTopologicalMackeyQuotientJacobian_ne_zero
        affineTopologicalMackeyQuotientJacobian_one
        affineTopologicalMackeyQuotientJacobian_cocycle
        (affineTopologicalMackeySectionPhase (xi := xi))
        (fun g ↦ (continuous_affineTopologicalMackeySectionPhase hxi g).aestronglyMeasurable)
        (fun g ↦ Filter.Eventually.of_forall
          (affineTopologicalMackeySectionPhase_norm_one hxi g))
        (affineTopologicalMackeySectionPhase_one hxi)
        (affineTopologicalMackeySectionPhase_cocycle hxi)
    The normalized-section realization of the unitary representation induced from the Mackey
    character.  The reentry factor is literally the inducing character applied to
    `s(q)⁻¹ g s(g⁻¹q)`; the quasi-invariant quotient measure supplies the independent
    Radon--Nikodym square-root correction. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_apply_ae_explicit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        fun q 
        LeanRidgelet.affineTopologicalMackeySectionPhase g q *
          ((NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g)) *
            f (g⁻¹  q))
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_apply_ae_explicit.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                    hxi)
                  g)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        fun q 
        LeanRidgelet.affineTopologicalMackeySectionPhase
            g q *
          ((NNReal.sqrt
                  (LeanRidgelet.affineTopologicalJacobian
                    g)) *
            f (g⁻¹  q))
    The normalized-section induced representation has the same explicit action, with the
    character of the reentry cocycle displayed through its equality with the Fourier phase. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_eq_quotient.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi =
        LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation
          hxi
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_eq_quotient.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi =
        LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation
          hxi
    The normalized-section induced model equals the explicit character-twisted quotient
    representation.  This closes the model-identification part of unitary induction; the remaining
    Mackey endpoint is the irreducibility/imprimitivity theorem itself. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_eq_transported.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi =
        LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
          hxi
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_eq_transported.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi =
        LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation
          hxi
    The normalized-section induced model is exactly the independently transported Fourier
    representation on the homogeneous quotient. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isStronglyContinuous.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).IsStronglyContinuous
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isStronglyContinuous.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).IsStronglyContinuous
    The normalized-section induced representation is strongly continuous. 
  • complete
    def LeanRidgelet.affineMackeySmoothedVector.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (MeasureTheory.Lp  2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineMackeySmoothedVector.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (MeasureTheory.Lp  2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi))
    Implementation after :=
    :=
      (affineTopologicalMackeySectionInducedLpUnitaryRepresentation hxi).haarIntegratedVector ψ f
    Folland's compactly supported convolution smoothing, expressed intrinsically as a Haar-
    integrated vector of the normalized-section induced representation. 
  • complete
    theorem LeanRidgelet.affineMackey_smoothing_integrable.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      MeasureTheory.Integrable
        (fun g 
          ψ g 
            ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                    hxi)
                  g)
              f)
        MeasureTheory.Measure.haar
    theorem LeanRidgelet.affineMackey_smoothing_integrable.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      MeasureTheory.Integrable
        (fun g 
          ψ g 
            ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                    hxi)
                  g)
              f)
        MeasureTheory.Measure.haar
    The orbit-kernel defining affine Mackey smoothing is Bochner integrable. 
  • complete
    theorem LeanRidgelet.affineMackeySmoothedVector_mem.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))}
      (hf : f  K) : LeanRidgelet.affineMackeySmoothedVector hxi ψ f  K
    theorem LeanRidgelet.affineMackeySmoothedVector_mem.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))}
      (hf : f  K) :
      LeanRidgelet.affineMackeySmoothedVector
          hxi ψ f 
        K
    Haar convolution smoothing preserves every closed subspace invariant under the induced
    representation. 
  • complete
    theorem LeanRidgelet.affineMackey_exists_smoothing_mem_tendsto.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))}
      (hf : f  K) :
       ψ,
        (∀ (n : ) (g : AffineEquiv.TopologicalSemidirectProduct E),
            0  (ψ n) g) 
          (∀ (n : ),
               (g : AffineEquiv.TopologicalSemidirectProduct E),
                  (ψ n) g MeasureTheory.Measure.haar =
                1) 
            (∀ U  nhds 1,
                ∀ᶠ (n : ) in Filter.atTop, tsupport (ψ n)  U) 
              (∀ (n : ),
                  LeanRidgelet.affineMackeySmoothedVector hxi
                      (UnitaryRepresentation.complexKernel (ψ n)) f 
                    K) 
                Filter.Tendsto
                  (fun n 
                    LeanRidgelet.affineMackeySmoothedVector hxi
                      (UnitaryRepresentation.complexKernel (ψ n)) f)
                  Filter.atTop (nhds f)
    theorem LeanRidgelet.affineMackey_exists_smoothing_mem_tendsto.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))}
      (hf : f  K) :
       ψ,
        (∀ (n : )
            (g :
              AffineEquiv.TopologicalSemidirectProduct
                E),
            0  (ψ n) g) 
          (∀ (n : ),
               (g :
                  AffineEquiv.TopologicalSemidirectProduct
                    E),
                  (ψ n)
                    g MeasureTheory.Measure.haar =
                1) 
            (∀ U  nhds 1,
                ∀ᶠ (n : ) in Filter.atTop,
                  tsupport (ψ n)  U) 
              (∀ (n : ),
                  LeanRidgelet.affineMackeySmoothedVector
                      hxi
                      (UnitaryRepresentation.complexKernel
                        (ψ n))
                      f 
                    K) 
                Filter.Tendsto
                  (fun n 
                    LeanRidgelet.affineMackeySmoothedVector
                      hxi
                      (UnitaryRepresentation.complexKernel
                        (ψ n))
                      f)
                  Filter.atTop (nhds f)
    Every vector in an invariant closed subspace is the `L²` limit of Haar-smoothed vectors in
    the same subspace, using compactly supported nonnegative probability kernels whose supports shrink
    to the identity.  This is the approximate-identity part of Folland Lemma 6.29. 
  • complete
    theorem LeanRidgelet.affineMackeySmoothedVector_exists_continuousRepresentative.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
       g,
        Continuous g 
          MeasureTheory.MemLp g 2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi) 
            (LeanRidgelet.affineMackeySmoothedVector hxi ψ
                    f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi]
              g
    theorem LeanRidgelet.affineMackeySmoothedVector_exists_continuousRepresentative.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
       g,
        Continuous g 
          MeasureTheory.MemLp g 2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi) 
            (LeanRidgelet.affineMackeySmoothedVector
                    hxi ψ
                    f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi]
              g
    Haar smoothing of the normalized-section induced model has a continuous representative on the
    homogeneous quotient.  A measurable representative of the quotient class lifts to the group so that
    the smoothing integral becomes a compact-kernel group convolution: the convolution is continuous by
    `LeanRidgelet.continuous_affineMackeySmoothingIntegral`, its slices over the finite-measure parts
    of the quotient are integrable by
    `LeanRidgelet.integrable_uncurry_affineMackeySmoothingIntegrand`, and
    `MeasureTheory.integral_L2_coeFn_ae_of_restrict` therefore identifies the `L²`-valued Bochner
    integral defining the smoothed vector with that pointwise integral.  The subsequent compact cutoff
    and density argument is proved below. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible_iff.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi).IsTopologicallyIrreducible 
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).IsTopologicallyIrreducible
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible_iff.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi).IsTopologicallyIrreducible 
        (LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume).IsTopologicallyIrreducible
    Mackey irreducibility for the normalized-section induced model is exactly the remaining
    irreducibility statement for the physical affine representation. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_indicator_covariant.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s) :
      let t := (fun q  g  q) ⁻¹' s;
      MeasureTheory.indicatorLp s hs ∘SL
          ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g) =
        ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g) ∘SL
          MeasureTheory.indicatorLp t 
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_indicator_covariant.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s) :
      let t := (fun q  g  q) ⁻¹' s;
      MeasureTheory.indicatorLp s hs ∘SL
          ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g) =
        ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g) ∘SL
          MeasureTheory.indicatorLp t 
    The measurable-set multiplication projections on the homogeneous quotient form the canonical
    system of imprimitivity for the normalized-section induced representation.  In operator form,
    restricting the output to `s` and then acting by `g` is the same as first restricting to the
    inverse translate of `s` and then acting by `g`. 
  • complete
    theorem LeanRidgelet.affineTopologicalTranslation_right.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (b : E) :
      ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
            (LeanRidgelet.affineTranslation b)).right =
        1
    theorem LeanRidgelet.affineTopologicalTranslation_right.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (b : E) :
      ((AffineEquiv.topologicalSemidirectProductEquiv
                E).symm
            (LeanRidgelet.affineTranslation
              b)).right =
        1
    In topological semidirect-product coordinates, a pure translation has identity linear
    coordinate. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyQuotient_translation_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0) (b : E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      (AffineEquiv.topologicalSemidirectProductEquiv E).symm
            (LeanRidgelet.affineTranslation b) 
          q =
        q
    theorem LeanRidgelet.affineTopologicalMackeyQuotient_translation_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0) (b : E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      (AffineEquiv.topologicalSemidirectProductEquiv
                E).symm
            (LeanRidgelet.affineTranslation
              b) 
          q =
        q
    The translation subgroup acts trivially on the affine homogeneous quotient.  This is the
    quotient-side form of the fact that the orbit map retains only the linear coordinate of an affine
    transformation. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) (b : E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      (((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                    hxi)
                  ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
                    (LeanRidgelet.affineTranslation b)))
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        fun q 
        ((LeanRidgelet.affineTranslationCharacter
                ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                      hxi)
                    q))
              b) *
          f q
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) (b : E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      (((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                    hxi)
                  ((AffineEquiv.topologicalSemidirectProductEquiv
                        E).symm
                    (LeanRidgelet.affineTranslation
                      b)))
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        fun q 
        ((LeanRidgelet.affineTranslationCharacter
                ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                      hxi)
                    q))
              b) *
          f q
    The restriction of the normalized-section induced representation to translations is the
    pointwise translation-character representation on the frequency orbit.  In particular, both the
    homogeneous-space motion and the Radon--Nikodym factor disappear; only the character at the
    frequency represented by the coset remains. 
  • complete
    def LeanRidgelet.affineTopologicalMackeyFrequencyEmbedding.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0) :
      LeanRidgelet.AffineTopologicalMackeyQuotient xi  E
    def LeanRidgelet.affineTopologicalMackeyFrequencyEmbedding.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0) :
      LeanRidgelet.AffineTopologicalMackeyQuotient
          xi 
        E
    Implementation after :=
    :=
      fun q ↦ (affineTopologicalMackeyQuotientHomeomorphDualOrbit hxi q).1
    The quotient-orbit coordinate, regarded as a measurable embedding into the ambient frequency
    space. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyFrequencyEmbedding_measurableEmbedding.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) :
      MeasurableEmbedding
        (LeanRidgelet.affineTopologicalMackeyFrequencyEmbedding hxi)
    theorem LeanRidgelet.affineTopologicalMackeyFrequencyEmbedding_measurableEmbedding.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      MeasurableEmbedding
        (LeanRidgelet.affineTopologicalMackeyFrequencyEmbedding
          hxi)
    The quotient-orbit coordinate is a measurable embedding. 
  • complete
    def LeanRidgelet.affineTopologicalMackeyTranslationMultiplier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) (b : E) :
      (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi)) ≃ₗᵢ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineTopologicalMackeyTranslationMultiplier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) (b : E) :
      (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi)) ≃ₗᵢ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    :=
      MeasureTheory.fourierCharacterLpMultiplier
        (μ := affineTopologicalMackeyQuotientMeasure hxi)
        (affineTopologicalMackeyFrequencyEmbedding hxi)
        (affineTopologicalMackeyFrequencyEmbedding_measurableEmbedding hxi).measurable b
    Multiplication by the character through which a pure translation acts on the Mackey
    quotient.  Bundling this operator separately makes the spectral-projection step independent of
    the group-representation implementation: its only input is commutation with these concrete
    Fourier-character multipliers. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyTranslationMultiplier_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) (b : E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      ((LeanRidgelet.affineTopologicalMackeyTranslationMultiplier hxi b)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        fun q 
        ((LeanRidgelet.affineTranslationCharacter
                ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                      hxi)
                    q))
              b) *
          f q
    theorem LeanRidgelet.affineTopologicalMackeyTranslationMultiplier_apply_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) (b : E)
      (f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))) :
      ((LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                hxi b)
              f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        fun q 
        ((LeanRidgelet.affineTranslationCharacter
                ((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                      hxi)
                    q))
              b) *
          f q
    The bundled Mackey translation multiplier has the expected pointwise representative. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_eq_multiplier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) (b : E) :
      ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi)
            ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
              (LeanRidgelet.affineTranslation b))) =
        (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier hxi b)
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_eq_multiplier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) (b : E) :
      ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi)
            ((AffineEquiv.topologicalSemidirectProductEquiv
                  E).symm
              (LeanRidgelet.affineTranslation
                b))) =
        (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
              hxi b)
    On the translation subgroup, the normalized-section induced representation is the concrete
    Mackey character multiplier. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_commutes_translation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hT :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          T)
      (b : E) :
      T ∘SL
          ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
                (LeanRidgelet.affineTranslation b))) =
        ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
                (LeanRidgelet.affineTranslation b))) ∘SL
          T
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_commutes_translation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hT :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          T)
      (b : E) :
      T ∘SL
          ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              ((AffineEquiv.topologicalSemidirectProductEquiv
                    E).symm
                (LeanRidgelet.affineTranslation
                  b))) =
        ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              ((AffineEquiv.topologicalSemidirectProductEquiv
                    E).symm
                (LeanRidgelet.affineTranslation
                  b))) ∘SL
          T
    An operator in the commutant of the induced affine representation commutes, in particular,
    with every member of its translation restriction.  Together with the preceding pointwise formula,
    this is the operator-theoretic input to the spectral-projection step. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_commutes_translationMultiplier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hT :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          T)
      (b : E) :
      T ∘SL
          (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier hxi
                b) =
        (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier hxi
                b) ∘SL
          T
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_commutes_translationMultiplier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hT :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          T)
      (b : E) :
      T ∘SL
          (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                hxi b) =
        (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                hxi b) ∘SL
          T
    An operator in the affine commutant therefore commutes with every concrete translation
    character multiplier. 
  • complete
    theorem LeanRidgelet.affineMackey_commutes_indicator_of_commutes_translation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (htranslation :
         (b : E),
          T ∘SL
              (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                    hxi b) =
            (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier hxi
                    b) ∘SL
              T)
      (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s) :
      T ∘SL MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL T
    theorem LeanRidgelet.affineMackey_commutes_indicator_of_commutes_translation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (htranslation :
         (b : E),
          T ∘SL
              (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                    hxi b) =
            (LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                    hxi b) ∘SL
              T)
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s) :
      T ∘SL MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL T
    Specialization of the commutant criterion in Folland Theorem 4.44 to the translation
    restriction of the affine induced model.  Since translations act by the characters displayed in
    `affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_apply_ae`, their spectral
    projections are the canonical measurable-set multiplication operators on the quotient orbit. 
  • complete
    theorem LeanRidgelet.affineMackey_indicatorLp_mem.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hindicator :
         (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection)
      (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s)
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))}
      (hf : f  K) : (MeasureTheory.indicatorLp s hs) f  K
    theorem LeanRidgelet.affineMackey_indicatorLp_mem.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hindicator :
        
          (s :
            Set
              (LeanRidgelet.AffineTopologicalMackeyQuotient
                xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL
              MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL
              (↑K).starProjection)
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s)
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))}
      (hf : f  K) :
      (MeasureTheory.indicatorLp s hs) f  K
    A system-invariant closed subspace is stable under every quotient-orbit indicator
    projection.  This is the elementary range-of-projection consequence used before the regular
    section argument of Folland Lemma 6.29. 
  • complete
    theorem LeanRidgelet.affineMackey_representation_mem.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))}
      (hf : f  K) :
      ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g)
          f 
        K
    theorem LeanRidgelet.affineMackey_representation_mem.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      {f :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))}
      (hf : f  K) :
      ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g)
          f 
        K
    A closed subspace whose star projection commutes with the induced representation is stable
    under the induced action. 
  • complete
    theorem LeanRidgelet.affineMackey_regularSection_memLp.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0)
      (f :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ) :
      MeasureTheory.MemLp (⇑f) 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)
    theorem LeanRidgelet.affineMackey_regularSection_memLp.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (f :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          ) :
      MeasureTheory.MemLp (⇑f) 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi)
    A compactly supported continuous scalar section on the homogeneous quotient belongs to
    `L²`. 
  • complete
    def LeanRidgelet.affineMackeyRegularSectionToLp.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0) :
      CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi)  →ₗ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    def LeanRidgelet.affineMackeyRegularSectionToLp.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
           →ₗ[]
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))
    Implementation after :=
    :=
      compactlySupportedContinuousToLp
    The linear map sending a regular quotient section to its `L²` class. 
  • complete
    def LeanRidgelet.affineMackeyRegularSectionEvaluation.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} :
      CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi)  →ₗ[]
        
    def LeanRidgelet.affineMackeyRegularSectionEvaluation.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} :
      CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
           →ₗ[]
        
    Implementation after :=
    := f (QuotientGroup.mk (1 : AffineEquiv.TopologicalSemidirectProduct E))
      map_add' f g := by simp
      map_smul' c f := by simp
    Evaluation of a regular section at the identity coset. 
  • complete
    def LeanRidgelet.affineMackeyRegularSectionsIn.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      Submodule 
        (CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) )
    def LeanRidgelet.affineMackeyRegularSectionsIn.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi))) :
      Submodule 
        (CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          )
    Implementation after :=
    :=
      K.toSubmodule.comap (affineMackeyRegularSectionToLp hxi)
    Regular sections whose `L²` classes belong to a fixed closed system-invariant subspace. 
  • complete
    def LeanRidgelet.affineMackeyInducingFiber.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      ClosedSubmodule  
    def LeanRidgelet.affineMackeyInducingFiber.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi))) :
      ClosedSubmodule  
    Implementation after :=
    :=
      (Submodule.map affineMackeyRegularSectionEvaluation
        (affineMackeyRegularSectionsIn hxi K)).closure
    The inducing fiber extracted from a closed subspace: take the closed linear span of the
    values at the identity coset of its regular sections.  This is the concrete scalar specialization
    of the fiber `M` constructed in Folland Lemma 6.30. 
  • complete
    theorem LeanRidgelet.affineMackey_regularSection_dense.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
         (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection) :
      Dense
        (Set.range fun f 
          (LeanRidgelet.affineMackeyRegularSectionToLp hxi) f, )
    theorem LeanRidgelet.affineMackey_regularSection_dense.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
        
          (s :
            Set
              (LeanRidgelet.AffineTopologicalMackeyQuotient
                xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL
              MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL
              (↑K).starProjection) :
      Dense
        (Set.range fun f 
          (LeanRidgelet.affineMackeyRegularSectionToLp
                hxi)
              f,
            )
    Folland Lemma 6.29 in the normalized quotient model: regular sections belonging to a closed
    subspace invariant under the system of imprimitivity are dense in that subspace. 
  • complete
    def LeanRidgelet.affineMackeyRegularSectionSMul.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ) :
      CompactlySupportedContinuousMap
        (LeanRidgelet.AffineTopologicalMackeyQuotient xi) 
    def LeanRidgelet.affineMackeyRegularSectionSMul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          ) :
      CompactlySupportedContinuousMap
        (LeanRidgelet.AffineTopologicalMackeyQuotient
          xi)
        
    Implementation after :=
    := affineTopologicalMackeySectionPhase g q *
        (((affineTopologicalJacobian g).sqrt : ℂ) * r (g⁻¹ • q))
      continuous_toFun :=
        (continuous_affineTopologicalMackeySectionPhase hxi g).mul
          (continuous_const.mul (r.continuous.comp (continuous_const_smul g⁻¹)))
      hasCompactSupport' := by
        have h : HasCompactSupport
            (fun q : AffineTopologicalMackeyQuotient xi ↦ r (g⁻¹ • q)) :=
          r.hasCompactSupport.comp_homeomorph (Homeomorph.smul g⁻¹)
        have heq : (fun q : AffineTopologicalMackeyQuotient xi ↦
              affineTopologicalMackeySectionPhase g q *
                (((affineTopologicalJacobian g).sqrt : ℂ) * r (g⁻¹ • q))) =
            (fun q : AffineTopologicalMackeyQuotient xi ↦
              affineTopologicalMackeySectionPhase g q *
                ((affineTopologicalJacobian g).sqrt : ℂ)) *
              fun q : AffineTopologicalMackeyQuotient xi ↦ r (g⁻¹ • q) := by
          funext q
          simp only [Pi.mul_apply, mul_assoc]
        rw [heq]
        exact h.mul_left
    Translating a compactly supported continuous quotient section by the induced action.  The
    phase and the Radon--Nikodym constant are unit-modulus and positive, so the translate is again a
    compactly supported continuous section. 
  • complete
    theorem LeanRidgelet.affineMackeyRegularSectionSMul_apply.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) )
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) :
      (LeanRidgelet.affineMackeyRegularSectionSMul hxi g r) q =
        LeanRidgelet.affineTopologicalMackeySectionPhase g q *
          ((NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g)) *
            r (g⁻¹  q))
    theorem LeanRidgelet.affineMackeyRegularSectionSMul_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          )
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      (LeanRidgelet.affineMackeyRegularSectionSMul
            hxi g r)
          q =
        LeanRidgelet.affineTopologicalMackeySectionPhase
            g q *
          ((NNReal.sqrt
                  (LeanRidgelet.affineTopologicalJacobian
                    g)) *
            r (g⁻¹  q))
  • complete
    theorem LeanRidgelet.affineMackeyRegularSectionToLp_coeFn_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ) :
      ((LeanRidgelet.affineMackeyRegularSectionToLp hxi)
              r) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        r
    theorem LeanRidgelet.affineMackeyRegularSectionToLp_coeFn_ae.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          ) :
      ((LeanRidgelet.affineMackeyRegularSectionToLp
                hxi)
              r) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        r
    A compactly supported continuous section represents its own `L²` class. 
  • complete
    theorem LeanRidgelet.affineMackeyRegularSectionToLp_smul.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) (g : AffineEquiv.TopologicalSemidirectProduct E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ) :
      (LeanRidgelet.affineMackeyRegularSectionToLp hxi)
          (LeanRidgelet.affineMackeyRegularSectionSMul hxi g r) =
        ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g)
          ((LeanRidgelet.affineMackeyRegularSectionToLp hxi) r)
    theorem LeanRidgelet.affineMackeyRegularSectionToLp_smul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          ) :
      (LeanRidgelet.affineMackeyRegularSectionToLp
            hxi)
          (LeanRidgelet.affineMackeyRegularSectionSMul
            hxi g r) =
        ((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              g)
          ((LeanRidgelet.affineMackeyRegularSectionToLp
              hxi)
            r)
    The `L²` class of a translated section is the induced action applied to the `L²` class of the
    section. 
  • complete
    theorem LeanRidgelet.affineMackeyRegularSectionSMul_ne_zero.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) )
      {q : LeanRidgelet.AffineTopologicalMackeyQuotient xi}
      (hq : r (g⁻¹  q)  0) :
      (LeanRidgelet.affineMackeyRegularSectionSMul hxi g r) q  0
    theorem LeanRidgelet.affineMackeyRegularSectionSMul_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          )
      {q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi}
      (hq : r (g⁻¹  q)  0) :
      (LeanRidgelet.affineMackeyRegularSectionSMul
            hxi g r)
          q 
        0
    The phase and Radon--Nikodym factors of the section model never vanish, so a translated section
    vanishes exactly where the original section does. 
  • complete
    theorem LeanRidgelet.affineMackeyRegularSection_eq_zero_of_smul_eq_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) )
      {q : LeanRidgelet.AffineTopologicalMackeyQuotient xi}
      (h : (LeanRidgelet.affineMackeyRegularSectionSMul hxi g r) q = 0) :
      r (g⁻¹  q) = 0
    theorem LeanRidgelet.affineMackeyRegularSection_eq_zero_of_smul_eq_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          )
      {q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi}
      (h :
        (LeanRidgelet.affineMackeyRegularSectionSMul
              hxi g r)
            q =
          0) :
      r (g⁻¹  q) = 0
    Vanishing of a translated section at the identity coset means vanishing of the section at the
    translated coset. 
  • complete
    theorem LeanRidgelet.affineMackeyInducingFiber_eq_bot_iff.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
      LeanRidgelet.affineMackeyInducingFiber hxi K =  
        
          (r :
            CompactlySupportedContinuousMap
              (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ),
          (LeanRidgelet.affineMackeyRegularSectionToLp hxi) r  K  r 1 = 0
    theorem LeanRidgelet.affineMackeyInducingFiber_eq_bot_iff.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi))) :
      LeanRidgelet.affineMackeyInducingFiber
            hxi K =
           
        
          (r :
            CompactlySupportedContinuousMap
              (LeanRidgelet.AffineTopologicalMackeyQuotient
                xi)
              ),
          (LeanRidgelet.affineMackeyRegularSectionToLp
                  hxi)
                r 
              K 
            r 1 = 0
    The inducing fiber is trivial exactly when every regular section of the subspace vanishes at
    the identity coset. 
  • complete
    theorem LeanRidgelet.affineMackeyInducingFiber_eq_top_of_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) )
      (hr : (LeanRidgelet.affineMackeyRegularSectionToLp hxi) r  K)
      (hr0 : r 1  0) : LeanRidgelet.affineMackeyInducingFiber hxi K = 
    theorem LeanRidgelet.affineMackeyInducingFiber_eq_top_of_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          )
      (hr :
        (LeanRidgelet.affineMackeyRegularSectionToLp
              hxi)
            r 
          K)
      (hr0 : r 1  0) :
      LeanRidgelet.affineMackeyInducingFiber
          hxi K =
        
    One regular section of the subspace that does not vanish at the identity coset already spans
    the whole one-dimensional inducing fiber. 
  • complete
    theorem LeanRidgelet.affineMackey_regularSection_eq_zero_of_inducingFiber_eq_bot.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hfiber : LeanRidgelet.affineMackeyInducingFiber hxi K = )
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) )
      (hr : (LeanRidgelet.affineMackeyRegularSectionToLp hxi) r  K)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) : r q = 0
    theorem LeanRidgelet.affineMackey_regularSection_eq_zero_of_inducingFiber_eq_bot.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hfiber :
        LeanRidgelet.affineMackeyInducingFiber
            hxi K =
          )
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          )
      (hr :
        (LeanRidgelet.affineMackeyRegularSectionToLp
              hxi)
            r 
          K)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      r q = 0
    If the inducing fiber is trivial, then every regular section of the subspace vanishes
    identically: the induced action moves the identity coset onto every coset, so the fiber condition
    propagates along the orbit. 
  • complete
    theorem LeanRidgelet.affineMackey_eq_bot_of_inducingFiber_eq_bot.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hregular :
        Dense
          (Set.range fun f 
            (LeanRidgelet.affineMackeyRegularSectionToLp hxi) f, ))
      (hfiber : LeanRidgelet.affineMackeyInducingFiber hxi K = ) : K = 
    theorem LeanRidgelet.affineMackey_eq_bot_of_inducingFiber_eq_bot.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hregular :
        Dense
          (Set.range fun f 
            (LeanRidgelet.affineMackeyRegularSectionToLp
                  hxi)
                f,
              ))
      (hfiber :
        LeanRidgelet.affineMackeyInducingFiber
            hxi K =
          ) :
      K = 
    A subspace with trivial inducing fiber is trivial.  Every regular section it contains vanishes
    identically, and regular sections are dense in it by the Folland-6.29 density theorem. 
  • complete
    theorem LeanRidgelet.affineMackey_eq_top_of_regularSection_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
         (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) )
      (hr : (LeanRidgelet.affineMackeyRegularSectionToLp hxi) r  K)
      (hr0 : r 1  0) : K = 
    theorem LeanRidgelet.affineMackey_eq_top_of_regularSection_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
        
          (s :
            Set
              (LeanRidgelet.AffineTopologicalMackeyQuotient
                xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL
              MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL
              (↑K).starProjection)
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          )
      (hr :
        (LeanRidgelet.affineMackeyRegularSectionToLp
              hxi)
            r 
          K)
      (hr0 : r 1  0) : K = 
    A subspace containing one regular section that does not vanish at the identity coset is
    everything.  Orthogonality to the subspace forces a vector to vanish almost everywhere on the
    nonvanishing set of every translate of that section, and countably many translates already cover the
    homogeneous quotient. 
  • complete
    theorem LeanRidgelet.affineMackey_closedSubspace_extreme_iff_inducingFiber_extreme.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
         (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection)
      (hregular :
        Dense
          (Set.range fun f 
            (LeanRidgelet.affineMackeyRegularSectionToLp hxi) f, )) :
      (K =   LeanRidgelet.affineMackeyInducingFiber hxi K = ) 
        (K =   LeanRidgelet.affineMackeyInducingFiber hxi K = )
    theorem LeanRidgelet.affineMackey_closedSubspace_extreme_iff_inducingFiber_extreme.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
        
          (s :
            Set
              (LeanRidgelet.AffineTopologicalMackeyQuotient
                xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL
              MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL
              (↑K).starProjection)
      (hregular :
        Dense
          (Set.range fun f 
            (LeanRidgelet.affineMackeyRegularSectionToLp
                  hxi)
                f,
              )) :
      (K =  
          LeanRidgelet.affineMackeyInducingFiber
              hxi K =
            ) 
        (K =  
          LeanRidgelet.affineMackeyInducingFiber
              hxi K =
            )
    Folland Lemma 6.30, restricted to the two conclusions needed for the one-dimensional affine
    inducing fiber.  The regular-section fiber is zero exactly when the induced closed subspace is
    zero, and it is the whole scalar fiber exactly when that subspace is the whole `L²` space.
    
    Both directions are assembled from the four lemmas above: identity-coset evaluation of translated
    sections for the zero case, together with the density hypothesis supplied by Folland 6.29, and
    orthogonal-complement vanishing along a countable subcover of translates for the full case. 
  • complete
    theorem LeanRidgelet.affineMackey_systemInvariant_closedSubspace_eq_bot_or_top.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
         (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection) :
      K =   K = 
    theorem LeanRidgelet.affineMackey_systemInvariant_closedSubspace_eq_bot_or_top.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (K :
        ClosedSubmodule 
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hrepresentation :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          (↑K).starProjection)
      (hindicator :
        
          (s :
            Set
              (LeanRidgelet.AffineTopologicalMackeyQuotient
                xi))
          (hs : MeasurableSet s),
          (↑K).starProjection ∘SL
              MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL
              (↑K).starProjection) :
      K =   K = 
    Folland Lemmas 6.29--6.30 for the canonical affine system with one-dimensional inducing
    fiber. A closed subspace whose orthogonal projection commutes with both the induced action and all
    quotient-orbit indicator projections is zero or the whole `L²` space.
    
    The regular-section density theorem above is a completed consequence of the named
    measurable-lift/product-integrability/convolution-formula placeholder, and the inducing-fiber
    correspondence is now proved. This theorem combines them with the proved classification of closed
    complex subspaces of the one-dimensional inducing fiber and contains no `sorry` of its own. 
  • complete
    theorem LeanRidgelet.affineMackey_scalar_of_commutes_indicators.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
      (hT :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          T)
      (hindicator :
         (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
          (hs : MeasurableSet s),
          T ∘SL MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL T) :
       c,
        T =
          c 
            ContinuousLinearMap.id 
              (MeasureTheory.Lp  2
                  (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
    theorem LeanRidgelet.affineMackey_scalar_of_commutes_indicators.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (T :
        (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)) →L[]
          (MeasureTheory.Lp  2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi)))
      (hT :
        (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
              hxi).Commutes
          T)
      (hindicator :
        
          (s :
            Set
              (LeanRidgelet.AffineTopologicalMackeyQuotient
                xi))
          (hs : MeasurableSet s),
          T ∘SL
              MeasureTheory.indicatorLp s hs =
            MeasureTheory.indicatorLp s hs ∘SL
              T) :
       c,
        T =
          c 
            ContinuousLinearMap.id 
              (MeasureTheory.Lp  2
                  (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                    hxi))
    Specialization of Folland Theorem 6.28 to the canonical affine system of imprimitivity.
    Commutation with the induced action and all quotient-orbit indicator projections identifies `T`
    with an operator in the commutant of the one-dimensional inducing character, hence with a scalar.
    
    The only unproved input is the Folland-6.29 smoothed-vector continuous-representative theorem
    used by the completed regular-section density argument. The spectral-subspace argument, the
    inducing-fiber correspondence, and the decomposition into two self-adjoint operators are proved
    here. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_hasSchurProperty.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).HasSchurProperty
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_hasSchurProperty.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).HasSchurProperty
    The assembled commutant form of the Mackey irreducibility step for the normalized-section
    induced model. An operator commuting with the induced affine action first commutes with the
    spectral projections of the translation subgroup, hence belongs to the commutant of the canonical
    system of imprimitivity; the imprimitivity commutant theorem then identifies it with the commutant
    of the inducing one-dimensional character, so it is scalar.
    
    All group, orbit, quotient-measure, section-cocycle, continuity, inducing-character,
    translation-spectral, and inducing-fiber inputs have already been constructed above. The remaining
    analytic input is the named Folland-6.29 smoothed-vector continuous-representative theorem used by
    the completed density argument; this assembly contains no source-level placeholder and uses no
    induction or imprimitivity assumptions structure.
    
  • complete
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).IsTopologicallyIrreducible
    theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0) :
      (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).IsTopologicallyIrreducible
    Folland Theorem 6.39, irreducibility direction, for the normalized-section affine induced
    model.  Once its commutant is scalar, the converse direction of the unitary Schur lemma turns the
    commutant statement into topological irreducibility. 
  • complete
    theorem LeanRidgelet.affineDataLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] :
      (LeanRidgelet.affineDataLpUnitaryRepresentation
          MeasureTheory.volume).IsTopologicallyIrreducible
    theorem LeanRidgelet.affineDataLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E] :
      (LeanRidgelet.affineDataLpUnitaryRepresentation
          MeasureTheory.volume).IsTopologicallyIrreducible
    Theorem 2.5 of arXiv:2405.13682: the scalar quasi-regular representation of the full affine
    group is topologically irreducible.
    
    The Fourier-conjugated representation has now been transported first to the intrinsic `L²` space
    on the conull nonzero-frequency subtype and then, through
    `affineTopologicalMackeyQuotientHomeomorphDualOrbit`, to the actual homogeneous-space
    `L²(G/H)`. Both transports have explicit inverse bounded intertwiners, and the homeomorphism is
    proved equivariant for left translation and the dual action. The closed locally compact inducing
    subgroup and its strongly continuous irreducible character representation are
    `affineTopologicalMackeySubgroup` and `affineTopologicalMackeyUnitaryRepresentation`, with the
    required translation and little-group restriction formulas.
    
    The normalized equivariant-section realization of unitary induction is now constructed explicitly:
    its reentry cocycle is `s(q)⁻¹ g s(g⁻¹q)`, its character phase is proved equal to the Fourier
    phase, and the resulting unitary representation is proved equal to the transported homogeneous
    model. The paper endpoint is derived from the commutant form of Folland Theorem 6.39 above. Its
    translation-spectral, spectral-subspace, compact-kernel convolution continuity, compact-cutoff,
    regular-section density, and 6.30 inducing-fiber inputs are complete, while its Folland-6.29
    measurable lift with product integrability and convolution formula is the one remaining HA
    placeholder. Mathlib's algebraic
    `Representation.ind` is not the quasi-invariant Hilbert-space construction and Mathlib has no
    imprimitivity theorem.
    

Inducing fiber. Translating a compactly supported continuous section by the induced action gives another such section, because the phase is continuous and unimodular, the Radon--Nikodym factor is a positive constant, and the shifted support is the homeomorphic image of a compact set; its L^2 class is the induced action applied to the original class. Since the transported quotient measure is positive on nonempty open sets, a section whose class vanishes vanishes identically, so a trivial subspace has a trivial fiber; conversely, if the fiber is trivial then evaluating translated sections at the identity coset kills a section at every coset, because the group acts transitively on the quotient, and regular-section density then forces the subspace to be trivial. A Urysohn bump provides a section with value one at the identity coset, so the full subspace has full fiber. If some section of the subspace does not vanish at the identity coset, then every vector orthogonal to the subspace vanishes almost everywhere on the nonvanishing set of each translate, by the indicator test of the Mathlib candidate layer; those nonvanishing sets are open and cover the quotient, second countability extracts a countable subcover, and the orthogonal complement is therefore zero. The combination of the two lemmas, the assembled Schur property, Schur's converse, and the model transports contain no further source-level sorry and derive the paper theorem.

Haar measure of the affine group along the orbit map

Theorem4.3.7
Statement uses 3
Statement dependency previews
Preview
Theorem 4.3.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

Quotient-integral input for the smoothing estimate. Local integrability of the lift of a quotient L^2 class needs an integral over a compact set of group elements to become an integral over a compact set of frequencies. The estimate proved here does exactly that: the image of a compactly restricted Haar measure of the affine group under the orbit map x\mapsto (x_{\mathrm{right}}^{-1})^\dagger\xi is dominated by a finite multiple of Lebesgue measure of frequency space, restricted to a compact set.

Lean code for Theorem4.3.79 declarations
  • complete
    def LeanRidgelet.affineLinearDeterminantCharacter.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] :
      (E →L[] E)ˣ →* ENNReal
    def LeanRidgelet.affineLinearDeterminantCharacter.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] :
      (E →L[] E)ˣ →* ENNReal
    Implementation after :=
    := ENNReal.ofReal |LinearMap.det ((L : E →L[ℝ] E) : E →ₗ[ℝ] E)|⁻¹
      map_one' := by simp
      map_mul' L M := by
        have hdet : LinearMap.det (((L * M : (E →L[ℝ] E)ˣ) : E →L[ℝ] E) : E →ₗ[ℝ] E) =
            LinearMap.det ((L : E →L[ℝ] E) : E →ₗ[ℝ] E) *
              LinearMap.det ((M : E →L[ℝ] E) : E →ₗ[ℝ] E) := by
          change LinearMap.det (((L : E →L[ℝ] E) ∘L (M : E →L[ℝ] E) : E →L[ℝ] E) : E →ₗ[ℝ] E) = _
          exact LinearMap.det_comp _ _
        rw [hdet, abs_mul, mul_inv, ENNReal.ofReal_mul (inv_nonneg.mpr (abs_nonneg _))]
    The reciprocal absolute determinant of the linear factor of the affine group, as a
    multiplicative character.  It is the factor by which the linear action rescales Lebesgue measure of
    the translation factor, hence the density that turns Haar measure of the linear factor into the
    relatively invariant measure of the semidirect-product factorization. 
  • complete
    theorem LeanRidgelet.affineLinearDeterminantCharacter_apply.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (L : (E →L[] E)ˣ) :
      LeanRidgelet.affineLinearDeterminantCharacter L =
        ENNReal.ofReal |LinearMap.det L|⁻¹
    theorem LeanRidgelet.affineLinearDeterminantCharacter_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (L : (E →L[] E)ˣ) :
      LeanRidgelet.affineLinearDeterminantCharacter
          L =
        ENNReal.ofReal |LinearMap.det L|⁻¹
  • complete
    theorem LeanRidgelet.affineLinearDeterminantCharacter_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] (L : (E →L[] E)ˣ) :
      LeanRidgelet.affineLinearDeterminantCharacter L  0
    theorem LeanRidgelet.affineLinearDeterminantCharacter_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      (L : (E →L[] E)ˣ) :
      LeanRidgelet.affineLinearDeterminantCharacter
          L 
        0
  • complete
    theorem LeanRidgelet.continuous_affineLinearDeterminantCharacter_real.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] : Continuous fun L  |LinearMap.det L|⁻¹
    theorem LeanRidgelet.continuous_affineLinearDeterminantCharacter_real.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] :
      Continuous fun L  |LinearMap.det L|⁻¹
  • complete
    theorem LeanRidgelet.measurable_affineLinearDeterminantCharacter.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace (E →L[] E)ˣ]
      [BorelSpace (E →L[] E)ˣ] :
      Measurable LeanRidgelet.affineLinearDeterminantCharacter
    theorem LeanRidgelet.measurable_affineLinearDeterminantCharacter.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace (E →L[] E)ˣ]
      [BorelSpace (E →L[] E)ˣ] :
      Measurable
        LeanRidgelet.affineLinearDeterminantCharacter
  • complete
    theorem LeanRidgelet.exists_affineLinearDeterminantCharacter_le_of_isCompact.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {K : Set (E →L[] E)ˣ} (hK : IsCompact K) :
       C,
        C     L  K, LeanRidgelet.affineLinearDeterminantCharacter L  C
    theorem LeanRidgelet.exists_affineLinearDeterminantCharacter_le_of_isCompact.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      {K : Set (E →L[] E)ˣ}
      (hK : IsCompact K) :
       C,
        C   
           L  K,
            LeanRidgelet.affineLinearDeterminantCharacter
                L 
              C
    On a compact set of linear factors the character is bounded. 
  • complete
    theorem LeanRidgelet.affine_map_orbitMap_haar_restrict_le.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi  0)
      {S : Set (AffineEquiv.TopologicalSemidirectProduct E)}
      (hS : IsCompact S) :
       C B,
        C   
          IsCompact B 
            MeasureTheory.Measure.map
                (LeanRidgelet.affineTopologicalMackeyOrbitMap xi)
                (MeasureTheory.Measure.haar.restrict S) 
              C  MeasureTheory.volume.restrict B
    theorem LeanRidgelet.affine_map_orbitMap_haar_restrict_le.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      {S :
        Set
          (AffineEquiv.TopologicalSemidirectProduct
            E)}
      (hS : IsCompact S) :
       C B,
        C   
          IsCompact B 
            MeasureTheory.Measure.map
                (LeanRidgelet.affineTopologicalMackeyOrbitMap
                  xi)
                (MeasureTheory.Measure.haar.restrict
                  S) 
              C 
                MeasureTheory.volume.restrict
                  B
    The image of a compactly restricted Haar measure of the affine group under the frequency orbit
    map is dominated by a finite multiple of Lebesgue measure of frequency space, restricted to the
    compact image.
    
    The translation factor contributes only the finite Haar measure of a compact set, because left
    translation acts on the two semidirect-product coordinates separately; the linear factor is handled
    by the contragredient-orbit estimate. 
  • complete
    theorem LeanRidgelet.affineTopologicalMackeyOrbitMap_inv.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (xi : E) (x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineTopologicalMackeyOrbitMap xi x⁻¹ =
        (ContinuousLinearMap.adjointEvalLinearMap E xi) x.right
    theorem LeanRidgelet.affineTopologicalMackeyOrbitMap_inv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (xi : E)
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineTopologicalMackeyOrbitMap
          xi x⁻¹ =
        (ContinuousLinearMap.adjointEvalLinearMap
            E xi)
          x.right
    The orbit map evaluated at an inverse is the adjoint orbit map: the linear coordinate of an
    inverse is the inverse linear coordinate, and the contragredient of an inverse is the adjoint. 
  • complete
    theorem LeanRidgelet.affine_map_adjointOrbitMap_haar_restrict_le.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0) {S : Set (AffineEquiv.TopologicalSemidirectProduct E)}
      (hS : IsCompact S) :
       C B,
        C   
          IsCompact B 
            MeasureTheory.Measure.map
                (fun x 
                  LeanRidgelet.affineTopologicalMackeyOrbitMap xi x⁻¹)
                (MeasureTheory.Measure.haar.restrict S) 
              C  MeasureTheory.volume.restrict B
    theorem LeanRidgelet.affine_map_adjointOrbitMap_haar_restrict_le.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      {S :
        Set
          (AffineEquiv.TopologicalSemidirectProduct
            E)}
      (hS : IsCompact S) :
       C B,
        C   
          IsCompact B 
            MeasureTheory.Measure.map
                (fun x 
                  LeanRidgelet.affineTopologicalMackeyOrbitMap
                    xi x⁻¹)
                (MeasureTheory.Measure.haar.restrict
                  S) 
              C 
                MeasureTheory.volume.restrict
                  B
    The same bound for the orbit map composed with inversion, which is the adjoint orbit map
    `x ↦ (x.right)† ξ`.  This is the form consumed by the group-convolution continuity theorem, whose
    local-integrability hypothesis is stated for the inverse-composed integrand.
    
    Taking adjoints is linear on the operator algebra, so this variant does not use the Haar transport
    along the contragredient automorphism. 

The same bound is proved for the orbit map composed with inversion, that is for the adjoint orbit map x\mapsto x_{\mathrm{right}}^\dagger\xi; that is the form the group-convolution continuity theorem consumes, since its local-integrability hypothesis is stated for the inverse-composed integrand. The proof instantiates the general semidirect-product factorization at the affine group and composes it with the contragredient-orbit estimate. The translation factor Multiplicative E is the additive group of E written multiplicatively, so its Haar measure is Lebesgue measure and the linear action rescales it by the reciprocal absolute determinant; that determinant is the multiplicative character of the factorization, continuous and nonvanishing, hence bounded on compact sets, which converts the relatively invariant measure of the linear factor back to Haar measure there. Borel structures on the two factors are introduced inside the proof rather than as global instances, since neither factor appears in the statement.

The equivariant lift to the group

Definition4.3.8
Statement uses 3
Statement dependency previews
Preview
Theorem 4.3.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

Lifting a quotient class to the group. Folland realizes an induced representation on functions over the group that transform by the inducing character, which turns smoothing into an ordinary group convolution. Here the lift multiplies a function on the quotient by the inverse section phase at the point itself, F(x)=P(x)^{-1}f(xH) with P(x)=\mathrm{phase}(x,xH).

Lean code for Definition4.3.822 declarations
  • complete
    def LeanRidgelet.affineMackeyLiftPhase.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (x : AffineEquiv.TopologicalSemidirectProduct E) : 
    def LeanRidgelet.affineMackeyLiftPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      
    Implementation after :=
    :=
      affineTopologicalMackeySectionPhase (xi := xi) x (QuotientGroup.mk x)
    The section phase of a group element at its own coset.  It is the gauge that makes the lift of a
    quotient function transform by the inducing character. 
  • complete
    theorem LeanRidgelet.affineMackeyLiftPhase_norm_one.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeyLiftPhase x = 1
    theorem LeanRidgelet.affineMackeyLiftPhase_norm_one.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeyLiftPhase x =
        1
  • complete
    theorem LeanRidgelet.affineMackeyLiftPhase_ne_zero.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeyLiftPhase x  0
    theorem LeanRidgelet.affineMackeyLiftPhase_ne_zero.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeyLiftPhase x  0
  • complete
    theorem LeanRidgelet.continuous_affineMackeyLiftPhase.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0) :
      Continuous LeanRidgelet.affineMackeyLiftPhase
    theorem LeanRidgelet.continuous_affineMackeyLiftPhase.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0) :
      Continuous
        LeanRidgelet.affineMackeyLiftPhase
    The lift phase is continuous: although the normalized section itself is only set-theoretic, its
    character equals the explicit Fourier phase, which is jointly continuous. 
  • complete
    theorem LeanRidgelet.affineMackeyLiftPhase_mul.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (g x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeyLiftPhase x =
        LeanRidgelet.affineTopologicalMackeySectionPhase g x *
          LeanRidgelet.affineMackeyLiftPhase (g⁻¹ * x)
    theorem LeanRidgelet.affineMackeyLiftPhase_mul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (g x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeyLiftPhase x =
        LeanRidgelet.affineTopologicalMackeySectionPhase
            g x *
          LeanRidgelet.affineMackeyLiftPhase
            (g⁻¹ * x)
    The cocycle law of the lift phase: translating the argument by `g⁻¹` splits off exactly the
    section phase of `g` at the coset. 
  • complete
    def LeanRidgelet.affineMackeyLiftFun.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  )
      (x : AffineEquiv.TopologicalSemidirectProduct E) : 
    def LeanRidgelet.affineMackeyLiftFun.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          )
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      
    Implementation after :=
    :=
      (affineMackeyLiftPhase (xi := xi) x)⁻¹ * f (QuotientGroup.mk x)
    The lift of a function on the affine homogeneous quotient to the affine group. 
  • complete
    theorem LeanRidgelet.affineMackeyLiftFun_apply.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  )
      (x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeyLiftFun f x =
        (LeanRidgelet.affineMackeyLiftPhase x)⁻¹ * f x
    theorem LeanRidgelet.affineMackeyLiftFun_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          )
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeyLiftFun f x =
        (LeanRidgelet.affineMackeyLiftPhase
              x)⁻¹ *
          f x
  • complete
    theorem LeanRidgelet.norm_affineMackeyLiftFun.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  )
      (x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeyLiftFun f x = f x
    theorem LeanRidgelet.norm_affineMackeyLiftFun.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          )
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeyLiftFun f x =
        f x
    The lift has the same absolute value as the function it lifts, because the gauge is
    unimodular. 
  • complete
    theorem LeanRidgelet.affineMackeyLiftFun_inv_mul.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      (f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  )
      (g x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeyLiftFun f (g⁻¹ * x) =
        (LeanRidgelet.affineMackeyLiftPhase x)⁻¹ *
          (LeanRidgelet.affineTopologicalMackeySectionPhase g x *
            f (g⁻¹  x))
    theorem LeanRidgelet.affineMackeyLiftFun_inv_mul.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          )
      (g x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeyLiftFun f
          (g⁻¹ * x) =
        (LeanRidgelet.affineMackeyLiftPhase
              x)⁻¹ *
          (LeanRidgelet.affineTopologicalMackeySectionPhase
              g x *
            f (g⁻¹  x))
    The translation identity that turns smoothing into a convolution: the lift at `g⁻¹ x` is the
    induced-action integrand at the coset of `x`, up to the gauge at `x`. 
  • complete
    theorem LeanRidgelet.measurable_affineMackeyLiftFun.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E} (hxi : xi  0)
      {f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  }
      (hf : Measurable f) : Measurable (LeanRidgelet.affineMackeyLiftFun f)
    theorem LeanRidgelet.measurable_affineMackeyLiftFun.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      {f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          }
      (hf : Measurable f) :
      Measurable
        (LeanRidgelet.affineMackeyLiftFun f)
    The lift of a measurable function is measurable: the gauge is continuous and the quotient map is
    continuous. 
  • complete
    theorem LeanRidgelet.affine_map_quotientMk_inv_haar_restrict_le.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      {S : Set (AffineEquiv.TopologicalSemidirectProduct E)}
      (hS : IsCompact S) :
       C B,
        C   
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi) B   
            MeasureTheory.Measure.map (fun x  x⁻¹)
                (MeasureTheory.Measure.haar.restrict S) 
              C 
                (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                      hxi).restrict
                  B
    theorem LeanRidgelet.affine_map_quotientMk_inv_haar_restrict_le.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      {S :
        Set
          (AffineEquiv.TopologicalSemidirectProduct
            E)}
      (hS : IsCompact S) :
       C B,
        C   
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                  hxi)
                B 
               
            MeasureTheory.Measure.map
                (fun x  x⁻¹)
                (MeasureTheory.Measure.haar.restrict
                  S) 
              C 
                (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                      hxi).restrict
                  B
    The image of a compactly restricted Haar measure of the affine group under the inverse coset
    map is dominated by a finite multiple of the homogeneous-quotient measure, restricted to a set of
    finite measure. 
  • complete
    theorem LeanRidgelet.locallyIntegrable_affineMackeyLiftFun_inv_of_bound.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      {f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  }
      (hfmeas : Measurable f)
      (hf :
        MeasureTheory.MemLp f 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))
      (hbound :
         (S : Set (AffineEquiv.TopologicalSemidirectProduct E)),
          IsCompact S 
             C B,
              C   
                (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)
                      B 
                     
                  MeasureTheory.Measure.map (fun x  x⁻¹)
                      (MeasureTheory.Measure.haar.restrict S) 
                    C 
                      (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                            hxi).restrict
                        B) :
      MeasureTheory.LocallyIntegrable
        (fun y  LeanRidgelet.affineMackeyLiftFun f y⁻¹)
        MeasureTheory.Measure.haar
    theorem LeanRidgelet.locallyIntegrable_affineMackeyLiftFun_inv_of_bound.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      {f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          }
      (hfmeas : Measurable f)
      (hf :
        MeasureTheory.MemLp f 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi))
      (hbound :
        
          (S :
            Set
              (AffineEquiv.TopologicalSemidirectProduct
                E)),
          IsCompact S 
             C B,
              C   
                (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                        hxi)
                      B 
                     
                  MeasureTheory.Measure.map
                      (fun x  x⁻¹)
                      (MeasureTheory.Measure.haar.restrict
                        S) 
                    C 
                      (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                            hxi).restrict
                        B) :
      MeasureTheory.LocallyIntegrable
        (fun y 
          LeanRidgelet.affineMackeyLiftFun f
            y⁻¹)
        MeasureTheory.Measure.haar
    The lift of an `L²` class on the affine homogeneous quotient, precomposed with inversion, is
    locally integrable on the affine group, provided the image of every compactly restricted Haar
    measure under `x ↦ x⁻¹ H` is dominated by a finite multiple of the homogeneous-space measure
    restricted to a set of finite measure.
    
    Local compactness reduces the claim to integrability on a compact set. The lift is measurable and
    has the same absolute value as the class it lifts, so the lower integral of its norm transports to
    the quotient along `x ↦ x⁻¹ H`; the domination hypothesis then bounds it by a finite multiple of
    the lower integral of `‖f‖` over a set of finite measure, which is finite because an `L²` function
    on a finite measure is integrable. 
  • complete
    theorem LeanRidgelet.locallyIntegrable_affineMackeyLiftFun_inv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      {f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  }
      (hfmeas : Measurable f)
      (hf :
        MeasureTheory.MemLp f 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)) :
      MeasureTheory.LocallyIntegrable
        (fun y  LeanRidgelet.affineMackeyLiftFun f y⁻¹)
        MeasureTheory.Measure.haar
    theorem LeanRidgelet.locallyIntegrable_affineMackeyLiftFun_inv.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      {f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          }
      (hfmeas : Measurable f)
      (hf :
        MeasureTheory.MemLp f 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)) :
      MeasureTheory.LocallyIntegrable
        (fun y 
          LeanRidgelet.affineMackeyLiftFun f
            y⁻¹)
        MeasureTheory.Measure.haar
    Local integrability of the lift composed with inversion, which is the hypothesis of the
    compact-kernel group-convolution continuity theorem.  It combines the quotient-form Haar
    pushforward bound with the Cauchy--Schwarz estimate on a finite-measure set. 
  • def LeanRidgelet.affineMackeySmoothingKernel.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E]
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) ) :
      CompactlySupportedContinuousMap
        (AffineEquiv.TopologicalSemidirectProduct E) 
    def LeanRidgelet.affineMackeySmoothingKernel.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          ) :
      CompactlySupportedContinuousMap
        (AffineEquiv.TopologicalSemidirectProduct
          E)
        
    Implementation after :=
    := ψ g * ((affineTopologicalJacobian g).sqrt : ℂ)
      continuous_toFun := by
        refine ψ.continuous.mul ?_
        exact Complex.continuous_ofReal.comp
          (NNReal.continuous_coe.comp
            (NNReal.continuous_sqrt.comp continuous_affineTopologicalJacobian))
      hasCompactSupport' := ψ.hasCompactSupport.mul_right
    The kernel of the smoothing integral, with the Radon--Nikodym square root absorbed. 
  • complete
    theorem LeanRidgelet.affineMackeySmoothingKernel_apply.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E]
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      (LeanRidgelet.affineMackeySmoothingKernel ψ) g =
        ψ g * (NNReal.sqrt (LeanRidgelet.affineTopologicalJacobian g))
    theorem LeanRidgelet.affineMackeySmoothingKernel_apply.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      (LeanRidgelet.affineMackeySmoothingKernel
            ψ)
          g =
        ψ g *
          (NNReal.sqrt
                (LeanRidgelet.affineTopologicalJacobian
                  g))
  • def LeanRidgelet.affineMackeySmoothingIntegrand.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E}
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      (f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  )
      (g : AffineEquiv.TopologicalSemidirectProduct E)
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) : 
    def LeanRidgelet.affineMackeySmoothingIntegrand.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      (f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          )
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E)
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      
    Implementation after :=
    :=
      ψ g * (affineTopologicalMackeySectionPhase g q *
        (((affineTopologicalJacobian g).sqrt : ℂ) * f (g⁻¹ • q)))
    The integrand of the smoothing integral, as a function of the group element and of the point of
    the homogeneous quotient.  Each slice in the group variable is the explicit almost-everywhere
    representative of the induced action, scaled by the smoothing kernel. 
  • complete
    theorem LeanRidgelet.measurable_uncurry_affineMackeySmoothingIntegrand.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      {f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  }
      (hfmeas : Measurable f) :
      Measurable
        (Function.uncurry (LeanRidgelet.affineMackeySmoothingIntegrand ψ f))
    theorem LeanRidgelet.measurable_uncurry_affineMackeySmoothingIntegrand.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      {f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          }
      (hfmeas : Measurable f) :
      Measurable
        (Function.uncurry
          (LeanRidgelet.affineMackeySmoothingIntegrand
            ψ f))
    The smoothing integrand is jointly measurable: every factor but `f` is jointly continuous, and
    `f` is composed with the continuous group action on the homogeneous quotient. 
  • complete
    theorem LeanRidgelet.affineMackeySmoothingIntegrand_ae_eq.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
      (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      {f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  }
      {F :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))}
      (hfF :
        f =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi] F)
      (g : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeySmoothingIntegrand ψ f
          g =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
        fun q 
        ψ g 
          (((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                        hxi)
                      g)
                  F)
            q
    theorem LeanRidgelet.affineMackeySmoothingIntegrand_ae_eq.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      {f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          }
      {F :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))}
      (hfF :
        f =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi]
          F)
      (g :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeySmoothingIntegrand
          ψ f
          g =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi]
        fun q 
        ψ g 
          (((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                        hxi)
                      g)
                  F)
            q
    Each slice of the smoothing integrand is almost everywhere the value of the kernel times the
    normalized-section induced action applied to the `L²` class that `f` represents. 
  • complete
    theorem LeanRidgelet.integrable_uncurry_affineMackeySmoothingIntegrand.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      {f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  }
      (hfmeas : Measurable f)
      {F :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))}
      (hfF :
        f =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi] F)
      {s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi)}
      (hs : MeasurableSet s)
      (hfin :
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi) s  ) :
      MeasureTheory.Integrable
        (Function.uncurry (LeanRidgelet.affineMackeySmoothingIntegrand ψ f))
        (MeasureTheory.Measure.haar.prod
          ((LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi).restrict
            s))
    theorem LeanRidgelet.integrable_uncurry_affineMackeySmoothingIntegrand.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      {f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          }
      (hfmeas : Measurable f)
      {F :
        (MeasureTheory.Lp  2
            (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi))}
      (hfF :
        f =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi]
          F)
      {s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)}
      (hs : MeasurableSet s)
      (hfin :
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
              hxi)
            s 
          ) :
      MeasureTheory.Integrable
        (Function.uncurry
          (LeanRidgelet.affineMackeySmoothingIntegrand
            ψ f))
        (MeasureTheory.Measure.haar.prod
          ((LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi).restrict
            s))
    The smoothing integrand is integrable on the product of the affine group with a finite-measure
    part of the homogeneous quotient.  Its slices are `L²` classes on the quotient, hence integrable on
    a set of finite measure, and Hölder's inequality bounds their `L¹` norms uniformly in the group
    variable because the induced action is unitary; the smoothing kernel then supplies a compactly
    supported dominating function on the group. 
  • def LeanRidgelet.affineMackeySmoothingIntegral.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      {xi : E}
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      (f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  )
      (q : LeanRidgelet.AffineTopologicalMackeyQuotient xi) : 
    def LeanRidgelet.affineMackeySmoothingIntegral.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      (f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          )
      (q :
        LeanRidgelet.AffineTopologicalMackeyQuotient
          xi) :
      
    Implementation after :=
    :=
      ∫ g, affineMackeySmoothingIntegrand ψ f g q ∂Measure.haar
    The pointwise smoothing integral on the homogeneous quotient. 
  • complete
    theorem LeanRidgelet.affineMackeySmoothingIntegral_quotientMk.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      (f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  )
      (x : AffineEquiv.TopologicalSemidirectProduct E) :
      LeanRidgelet.affineMackeySmoothingIntegral ψ f x =
        LeanRidgelet.affineMackeyLiftPhase x *
           (y : AffineEquiv.TopologicalSemidirectProduct E),
            LeanRidgelet.affineMackeyLiftFun f y⁻¹ *
              (LeanRidgelet.affineMackeySmoothingKernel ψ)
                (x * y) MeasureTheory.Measure.haar
    theorem LeanRidgelet.affineMackeySmoothingIntegral_quotientMk.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      (f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          )
      (x :
        AffineEquiv.TopologicalSemidirectProduct
          E) :
      LeanRidgelet.affineMackeySmoothingIntegral
          ψ f x =
        LeanRidgelet.affineMackeyLiftPhase x *
           (y :
            AffineEquiv.TopologicalSemidirectProduct
              E),
            LeanRidgelet.affineMackeyLiftFun f
                y⁻¹ *
              (LeanRidgelet.affineMackeySmoothingKernel
                  ψ)
                (x *
                  y) MeasureTheory.Measure.haar
    The smoothing integral along the quotient map is the group convolution of the smoothing kernel
    with the lift, corrected by the gauge.  This is the identity that makes the convolution continuity
    theorem applicable. 
  • complete
    theorem LeanRidgelet.continuous_affineMackeySmoothingIntegral.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E} (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct E) )
      {f : LeanRidgelet.AffineTopologicalMackeyQuotient xi  }
      (hloc :
        MeasureTheory.LocallyIntegrable
          (fun y  LeanRidgelet.affineMackeyLiftFun f y⁻¹)
          MeasureTheory.Measure.haar) :
      Continuous (LeanRidgelet.affineMackeySmoothingIntegral ψ f)
    theorem LeanRidgelet.continuous_affineMackeySmoothingIntegral.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] {xi : E}
      (hxi : xi  0)
      (ψ :
        CompactlySupportedContinuousMap
          (AffineEquiv.TopologicalSemidirectProduct
            E)
          )
      {f :
        LeanRidgelet.AffineTopologicalMackeyQuotient
            xi 
          }
      (hloc :
        MeasureTheory.LocallyIntegrable
          (fun y 
            LeanRidgelet.affineMackeyLiftFun f
              y⁻¹)
          MeasureTheory.Measure.haar) :
      Continuous
        (LeanRidgelet.affineMackeySmoothingIntegral
          ψ f)
    Continuity of the smoothing integral on the homogeneous quotient, given local integrability of
    the lift.  The convolution is continuous by the compact-kernel group-convolution theorem, the gauge
    is continuous, and the quotient map is a topological quotient map. 

The gauge P is unimodular, nowhere zero, and continuous — although the normalized section is only set-theoretic, its character equals the explicit Fourier phase, and that phase is continuous in both arguments. The cocycle law of the section phase gives P(x)=\mathrm{phase}(g,xH)\,P(g^{-1}x), hence the translation identity F(g^{-1}x)=P(x)^{-1}\bigl(\mathrm{phase}(g,xH)\,f(g^{-1}\cdot xH)\bigr), whose right-hand side is exactly the integrand of the induced action at the coset of x, up to the factor P(x)^{-1} that does not depend on the integration variable. Convolving with a compactly supported kernel therefore reproduces the smoothed vector along the quotient map, and continuity of the convolution transfers to the quotient because the quotient map is a topological quotient map. Absolute values of the lift are those of the original function, which is what the local-integrability estimate consumes.

The estimate and the lift combine into continuity of the smoothing integral. Transporting the frequency-space Haar bound along the quotient-orbit homeomorphism gives the same bound on the homogeneous quotient, and Cauchy--Schwarz on a finite-measure set turns it into local integrability of the lift composed with inversion — exactly the hypothesis of the compact-kernel group-convolution theorem. Along the quotient map the smoothing integral is that convolution, of the compactly supported kernel ψ\cdot\sqrt{\det} with the lift, corrected by the continuous unimodular gauge; hence it is continuous on the group, and it descends because the quotient map of a topological group by a subgroup is a quotient map.

What is left for Lemma 6.29 is to know that this pointwise integral is the representative of the Bochner-integrated vector, and that is a slice-integrability question. Each slice of the smoothing integrand in the group variable is, almost everywhere, the value of the kernel times the induced action applied to the class of the data, so all slices have the same L^2 norm; on a set of finite measure Hölder's inequality turns that into a uniform bound on their L^1 norms, and the compactly supported kernel dominates the group variable. The integrand is jointly measurable because the section phase is jointly continuous in the group element and the coset. The family is therefore integrable on the product of the group with every finite-measure part of the quotient, which is exactly the hypothesis of the slice form of the pointwise-representative theorem: a measurable representative of the data yields a continuous representative of the smoothed vector, and the Lemma 6.29 root is closed.