Documentation

Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Definition of BoundedContinuousFunction.char #

Definition and basic properties of BoundedContinuousFunction.char he hL w := fun v ↦ e (L v w), where e is a continuous additive character and L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ is a continuous bilinear map.

In the special case e = Circle.exp, this is used to define the characteristic function of a measure.

Main definitions #

Main statements #

def BoundedContinuousFunction.char {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } (he : Continuous e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (w : W) :

The bounded continuous mapping fun v ↦ e (L v w) from V to .

Equations
Instances For
    @[simp]
    theorem BoundedContinuousFunction.char_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} (w : W) (v : V) :
    (char he hL w) v = (e ((L v) w))
    @[simp]
    theorem BoundedContinuousFunction.char_zero_eq_one {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} :
    char he hL 0 = 1
    theorem BoundedContinuousFunction.char_add_eq_mul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} (x y : W) :
    char he hL (x + y) = char he hL x * char he hL y
    theorem BoundedContinuousFunction.char_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} (w : W) :
    char he hL (-w) = star (char he hL w)
    theorem BoundedContinuousFunction.ext_of_char_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } (he : Continuous e) (he' : e 1) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hL' : ∀ (v : V), v 0L v 0) {v v' : V} (h : ∀ (w : W), (char he hL w) v = (char he hL w) v') :
    v = v'

    If e and L are non-trivial, then char he hL w, w : W separates points in V.

    Monoid homomorphism mapping w to fun v ↦ e (L v w).

    Equations
    Instances For
      @[simp]
      theorem BoundedContinuousFunction.charMonoidHom_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} (w : Multiplicative W) (v : V) :
      ((charMonoidHom he hL) w) v = (e ((L v) w))

      Algebra homomorphism mapping w to fun v ↦ e (L v w).

      Equations
      Instances For
        @[simp]
        theorem BoundedContinuousFunction.charAlgHom_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} (w : AddMonoidAlgebra W) (v : V) :
        ((charAlgHom he hL) w) v = aw.support, w a * (e ((L v) a))
        theorem BoundedContinuousFunction.star_mem_range_charAlgHom {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } (he : Continuous e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {x : BoundedContinuousFunction V } (hx : x (charAlgHom he hL).range) :

        The family of -linear combinations of char he hL w, w : W, is closed under star.

        noncomputable def BoundedContinuousFunction.charPoly {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } (he : Continuous e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) :

        The star-subalgebra of polynomials.

        Equations
        Instances For
          theorem BoundedContinuousFunction.mem_charPoly {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} (f : BoundedContinuousFunction V ) :
          f charPoly he hL ∃ (w : AddMonoidAlgebra W), f = fun (x : V) => aw.support, w a * (e ((L x) a))
          theorem BoundedContinuousFunction.char_mem_charPoly {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } {he : Continuous e} {hL : Continuous fun (p : V × W) => (L p.1) p.2} (w : W) :
          char he hL w charPoly he hL
          theorem BoundedContinuousFunction.separatesPoints_charPoly {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module V] [TopologicalSpace V] [AddCommGroup W] [Module W] [TopologicalSpace W] {e : AddChar Circle} {L : V →ₗ[] W →ₗ[] } (he : Continuous e) (he' : e 1) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hL' : ∀ (v : V), v 0L v 0) :

          The family charPoly he hL w, w : W separates points in V.