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 mappingfun v ↦ e (L v w)
fromV
toℂ
, wheree
is a continuous additive character andL : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
is a continuous bilinear map.charPoly he hL : W → ℂ
: TheStarSubalgebra ℂ (V →ᵇ ℂ)
consisting ofℂ
-linear combinations ofchar he hL w
, wherew : W
.
Main statements #
ext_of_char_eq
: Ife
andL
are non-trivial, thenchar he hL w, w : W
separates points inV
.star_mem_range_charAlgHom
: The family ofℂ
-linear combinations ofchar he hL w, w : W
, is closed understar
.separatesPoints_charPoly
: The familycharPoly he hL w, w : W
separates points inV
.
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
- BoundedContinuousFunction.char he hL w = { toFun := fun (v : V) => ↑(e ((L v) w)), continuous_toFun := ⋯, map_bounded' := ⋯ }
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)
:
@[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}
:
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)
:
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)
:
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')
:
If e
and L
are non-trivial, then char he hL w, w : W
separates points in V
.
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)
:
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
@[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)
:
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)
:
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)
:
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
- BoundedContinuousFunction.charPoly he hL = { toSubalgebra := (BoundedContinuousFunction.charAlgHom he hL).range, star_mem' := ⋯ }
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 ℂ)
:
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)
:
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
.