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.

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 ℂ.

@[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 ≠ 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.

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).

@[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) (Multiplicative.toAdd w)))

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).

@[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 = w.coeff.sum fun (a : W) (z : ℂ) => z • ↑(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) : star 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) : StarSubalgebra ℂ (BoundedContinuousFunction V ℂ)

The star-subalgebra of polynomials.

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) => w.coeff.sum fun (a : W) (z : ℂ) => z * ↑(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 ≠ 0 → L v ≠ 0) : (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL)).SeparatesPoints

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