# 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 #

- `char he hL w : V →ᵇ ℂ`: Bounded continuous mapping `fun v ↦ e (L v w)` from `V` to `ℂ`, where `e` is a continuous additive character and `L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ` is a continuous bilinear map.
- `charPoly he hL : W → ℂ`: The `StarSubalgebra ℂ (V →ᵇ ℂ)` consisting of `ℂ`-linear combinations of `char he hL w`, where `w : W`.

## Main statements #

- `ext_of_char_eq`: If `e` and `L` are non-trivial, then `char he hL w, w : W` separates points in `V`.
- `star_mem_range_charAlgHom`: The family of `ℂ`-linear combinations of `char he hL w, w : W`, is closed under `star`.
- `separatesPoints_charPoly`: The family `charPoly he hL w, w : W` separates points in `V`.

source
noncomputable 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) :
BoundedContinuousFunction V ℂ

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

Equations

- BoundedContinuousFunction.char he hL w = { toFun := fun (v : V) => ↑(e ((L v) w)), continuous_toFun := ⋯, map_bounded' := ⋯ }

Instances For

source
@[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))
source
@[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
source
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
source
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)
source
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 ≠ 0 → L 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`.

source
noncomputable def BoundedContinuousFunction.charMonoidHom {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) :
Multiplicative W →* BoundedContinuousFunction V ℂ

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

Equations

- BoundedContinuousFunction.charMonoidHom he hL = { toFun := fun (w : Multiplicative W) => BoundedContinuousFunction.char he hL w, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[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))
source
noncomputable def BoundedContinuousFunction.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) :
AddMonoidAlgebra ℂ W →ₐ[ℂ] BoundedContinuousFunction V ℂ

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

Equations

- BoundedContinuousFunction.charAlgHom he hL = (AddMonoidAlgebra.lift ℂ W (BoundedContinuousFunction V ℂ)) (BoundedContinuousFunction.charMonoidHom he hL)

Instances For

source
@[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 = ∑ a ∈ w.support, w a * ↑(e ((L v) a))
source
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) :
star x ∈ (charAlgHom he hL).range

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

source
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) :
StarSubalgebra ℂ (BoundedContinuousFunction V ℂ)

The star-subalgebra of polynomials.

Equations

- BoundedContinuousFunction.charPoly he hL = { toSubalgebra := (BoundedContinuousFunction.charAlgHom he hL).range, star_mem' := ⋯ }

Instances For

source
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) => ∑ a ∈ w.support, w a * ↑(e ((L x) a))
source
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
source
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 ≠ 0 → L v ≠ 0) :
(StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL)).SeparatesPoints

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