# Characteristic Function of a Finite Measure #

This file defines the characteristic function of a finite measure on a topological vector space `V`.

The characteristic function of a finite measure `P` on `V` is the mapping `W → ℂ, w => ∫ v, e (L v w) ∂P`, where `e` is a continuous additive character and `L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ` is a bilinear map.

A typical example is `V = W = ℝ` and `L v w = v * w`.

The integral is expressed as `∫ v, char he hL w v ∂P`, where `char he hL w` is the bounded continuous function `fun v ↦ e (L v w)` and `he`, `hL` are continuity hypotheses on `e` and `L`.

## Main definitions #

- `innerProbChar`: the bounded continuous map `x ↦ exp(⟪x, t⟫ * I)` in an inner product space. This is `char` for the inner product bilinear map and the additive character `e = probChar`.
- `charFun μ t`: the characteristic function of a measure `μ` at `t` in an inner product space `E`. This is defined as `∫ x, exp (⟪x, t⟫ * I) ∂μ`, where `⟪x, t⟫` is the inner product on `E`. It is equal to `∫ v, innerProbChar w v ∂P` (see `charFun_eq_integral_innerProbChar`).
- `probCharDual`: the bounded continuous map `x ↦ exp (L x * I)`, for a continuous linear form `L`.
- `charFunDual μ L`: the characteristic function of a measure `μ` at `L : Dual ℝ E` in a normed space `E`. This is the integral `∫ v, exp (L v * I) ∂μ`.

## Main statements #

- `ext_of_integral_char_eq`: Assume `e` and `L` are non-trivial. If the integrals of `char` with respect to two finite measures `P` and `P'` coincide, then `P = P'`.
- `Measure.ext_of_charFun`: If the characteristic functions `charFun` of two finite measures `μ` and `ν` on a complete second-countable inner product space coincide, then `μ = ν`.
- `Measure.ext_of_charFunDual`: If the characteristic functions `charFunDual` of two finite measures `μ` and `ν` on a Banach space coincide, then `μ = ν`.

source
noncomputable def BoundedContinuousFunction.innerProbChar {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) :
BoundedContinuousFunction E ℂ

The bounded continuous map `x ↦ exp(⟪x, t⟫ * I)`.

Equations

- BoundedContinuousFunction.innerProbChar t = BoundedContinuousFunction.char Real.continuous_probChar ⋯ t

Instances For

source
theorem BoundedContinuousFunction.innerProbChar_apply {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t x : E) :
(innerProbChar t) x = Complex.exp (↑(inner ℝ x t) * Complex.I)
source
@[simp]
theorem BoundedContinuousFunction.innerProbChar_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] :
innerProbChar 0 = 1
source
noncomputable def BoundedContinuousFunction.probCharDual {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace ℝ F] (L : StrongDual ℝ F) :
BoundedContinuousFunction F ℂ

The bounded continuous map `x ↦ exp (L x * I)`, for a continuous linear form `L`.

Equations

- BoundedContinuousFunction.probCharDual L = BoundedContinuousFunction.char Real.continuous_probChar ⋯ L

Instances For

source
theorem BoundedContinuousFunction.probCharDual_apply {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace ℝ F] (L : StrongDual ℝ F) (x : F) :
(probCharDual L) x = Complex.exp (↑(L x) * Complex.I)
source
@[simp]
theorem BoundedContinuousFunction.probCharDual_zero {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace ℝ F] :
probCharDual 0 = 1
source
theorem MeasureTheory.ext_of_integral_char_eq {W : Type u_1} [AddCommGroup W] [Module ℝ W] [TopologicalSpace W] {e : AddChar ℝ Circle} {V : Type u_2} [AddCommGroup V] [Module ℝ V] [PseudoEMetricSpace V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace V] [SecondCountableTopology V] {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e) (he' : e ≠ 1) (hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {P P' : Measure V} [IsFiniteMeasure P] [IsFiniteMeasure P'] (h : ∀ (w : W), ∫ (v : V), (BoundedContinuousFunction.char he hL w) v ∂P = ∫ (v : V), (BoundedContinuousFunction.char he hL w) v ∂P') :
P = P'

If the integrals of `char` with respect to two finite measures `P` and `P'` coincide, then `P = P'`.

source
noncomputable def MeasureTheory.charFun {E : Type u_2} {mE : MeasurableSpace E} [Inner ℝ E] (μ : Measure E) (t : E) :
ℂ

The characteristic function of a measure in an inner product space.

Equations

- MeasureTheory.charFun μ t = ∫ (x : E), Complex.exp (↑(inner ℝ x t) * Complex.I) ∂μ

Instances For

source
theorem MeasureTheory.charFun_apply {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [Inner ℝ E] (t : E) :
charFun μ t = ∫ (x : E), Complex.exp (↑(inner ℝ x t) * Complex.I) ∂μ
source
theorem MeasureTheory.charFun_apply_real {μ : Measure ℝ} (t : ℝ) :
charFun μ t = ∫ (x : ℝ), Complex.exp (↑t * ↑x * Complex.I) ∂μ
source
@[simp]
theorem MeasureTheory.charFun_zero {E : Type u_2} {mE : MeasurableSpace E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : Measure E) :
charFun μ 0 = ↑(μ.real Set.univ)
source
@[simp]
theorem MeasureTheory.charFun_zero_measure {E : Type u_2} {mE : MeasurableSpace E} {t : E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] :
charFun 0 t = 0
source
@[simp]
theorem MeasureTheory.charFun_neg {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) :
charFun μ (-t) = (starRingEnd ℂ) (charFun μ t)
source
theorem MeasureTheory.charFun_eq_integral_innerProbChar {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} {t : E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] :
charFun μ t = ∫ (v : E), (BoundedContinuousFunction.innerProbChar t) v ∂μ

`charFun` as the integral of a bounded continuous function.

source
theorem MeasureTheory.charFun_eq_integral_probChar {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) :
charFun μ t = ∫ (x : E), ↑(Real.probChar (inner ℝ x t)) ∂μ
source
theorem MeasureTheory.charFun_eq_fourierIntegral {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) :
charFun μ t = VectorFourier.fourierIntegral Real.probChar μ bilinFormOfRealInner 1 (-t)

`charFun` is a Fourier integral for the inner product and the character `probChar`.

source
theorem MeasureTheory.charFun_eq_fourierIntegral' {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) :
charFun μ t = VectorFourier.fourierIntegral Real.fourierChar μ bilinFormOfRealInner 1 (-(2 * Real.pi)⁻¹ • t)

`charFun` is a Fourier integral for the inner product and the character `fourierChar`.

source
theorem MeasureTheory.norm_charFun_le {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) :
‖charFun μ t‖ ≤ μ.real Set.univ
source
theorem MeasureTheory.norm_charFun_le_one {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [IsProbabilityMeasure μ] (t : E) :
‖charFun μ t‖ ≤ 1
source
theorem MeasureTheory.norm_one_sub_charFun_le_two {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} {t : E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [IsProbabilityMeasure μ] :
‖1 - charFun μ t‖ ≤ 2
source
theorem MeasureTheory.stronglyMeasurable_charFun {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [OpensMeasurableSpace E] [SecondCountableTopology E] [SFinite μ] :
StronglyMeasurable (charFun μ)
source
theorem MeasureTheory.measurable_charFun {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [OpensMeasurableSpace E] [SecondCountableTopology E] [SFinite μ] :
Measurable (charFun μ)
source
theorem MeasureTheory.intervalIntegrable_charFun {μ : Measure ℝ} [IsFiniteMeasure μ] {a b : ℝ} :
IntervalIntegrable (charFun μ) volume a b
source
theorem MeasureTheory.charFun_map_smul {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] (r : ℝ) (t : E) :
charFun (Measure.map (fun (x : E) => r • x) μ) t = charFun μ (r • t)
source
theorem MeasureTheory.charFun_map_mul {μ : Measure ℝ} (r t : ℝ) :
charFun (Measure.map (fun (x : ℝ) => r * x) μ) t = charFun μ (r * t)
source
@[simp]
theorem MeasureTheory.charFun_dirac {E : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [OpensMeasurableSpace E] {x : E} (t : E) :
charFun (Measure.dirac x) t = Complex.exp (↑(inner ℝ x t) * Complex.I)
source
theorem MeasureTheory.charFun_map_add_const {E : Type u_3} [MeasurableSpace E] {μ : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] (r t : E) :
charFun (Measure.map (fun (x : E) => x + r) μ) t = charFun μ t * Complex.exp (↑(inner ℝ r t) * Complex.I)
source
theorem MeasureTheory.charFun_map_const_add {E : Type u_3} [MeasurableSpace E] {μ : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] (r t : E) :
charFun (Measure.map (fun (x : E) => r + x) μ) t = charFun μ t * Complex.exp (↑(inner ℝ r t) * Complex.I)
source
theorem MeasureTheory.Measure.ext_of_charFun {E : Type u_3} [MeasurableSpace E] {μ ν : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : charFun μ = charFun ν) :
μ = ν

If the characteristic functions `charFun` of two finite measures `μ` and `ν` on a complete second-countable inner product space coincide, then `μ = ν`.

source
theorem MeasureTheory.charFun_conv {E : Type u_3} [MeasurableSpace E] {μ ν : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] [IsFiniteMeasure μ] [IsFiniteMeasure ν] (t : E) :
charFun (μ.conv ν) t = charFun μ t * charFun ν t

The characteristic function of a convolution of measures is the product of the respective characteristic functions.

source
theorem MeasureTheory.charFun_prod {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {mE : MeasurableSpace E} {mF : MeasurableSpace F} {μ : Measure E} {ν : Measure F} [SFinite μ] [SFinite ν] (t : WithLp 2 (E × F)) :
charFun (Measure.map (WithLp.toLp 2) (μ.prod ν)) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2

The characteristic function of a product of measures is a product of characteristic functions. This is the version for Hilbert spaces, see `charFunDual_prod` for the Banach space version.

source
theorem MeasureTheory.charFun_eq_prod_iff {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {mE : MeasurableSpace E} {mF : MeasurableSpace F} [CompleteSpace E] [CompleteSpace F] [SecondCountableTopology E] [SecondCountableTopology F] [BorelSpace E] [BorelSpace F] {μ : Measure E} {ν : Measure F} {ξ : Measure (E × F)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteMeasure ξ] :
(∀ (t : WithLp 2 (E × F)), charFun (Measure.map (WithLp.toLp 2) ξ) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2) ↔ ξ = μ.prod ν

The characteristic function of a measure is a product of characteristic functions if and only if it is a product measure. This is the version for Hilbert spaces, see `charFunDual_eq_prod_iff` for the Banach space version.

source
theorem MeasureTheory.charFun_pi {ι : Type u_6} [Fintype ι] {E : ι → Type u_7} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → Measure (E i)} [∀ (i : ι), SigmaFinite (μ i)] (t : PiLp 2 E) :
charFun (Measure.map (WithLp.toLp 2) (Measure.pi μ)) t = ∏ i : ι, charFun (μ i) (t.ofLp i)

The characteristic function of a product of measures is a product of characteristic functions. This is the version for Hilbert spaces, see `charFunDual_pi` for the Banach space version.

source
theorem MeasureTheory.charFun_eq_pi_iff {ι : Type u_6} [Fintype ι] {E : ι → Type u_7} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] [∀ (i : ι), BorelSpace (E i)] {μ : (i : ι) → Measure (E i)} {ν : Measure ((i : ι) → E i)} [∀ (i : ι), IsFiniteMeasure (μ i)] [IsFiniteMeasure ν] :
(∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (WithLp.toLp 2) ν) t = ∏ i : ι, charFun (μ i) (t.ofLp i)) ↔ ν = Measure.pi μ

The characteristic function of a measure is a product of characteristic functions if and only if it is a product measure. This is the version for Hilbert spaces, see `charFunDual_eq_pi_iff` for the Banach space version.

source
noncomputable def MeasureTheory.charFunDual {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} (μ : Measure E) (L : StrongDual ℝ E) :
ℂ

The characteristic function of a measure in a normed space, function from `StrongDual ℝ E` to `ℂ` with `charFunDual μ L = ∫ v, exp (L v * I) ∂μ`.

Equations

- MeasureTheory.charFunDual μ L = ∫ (v : E), (BoundedContinuousFunction.probCharDual L) v ∂μ

Instances For

source
theorem MeasureTheory.charFunDual_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} (L : StrongDual ℝ E) :
charFunDual μ L = ∫ (v : E), Complex.exp (↑(L v) * Complex.I) ∂μ
source
theorem MeasureTheory.charFunDual_eq_charFun_map_one {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [OpensMeasurableSpace E] (L : StrongDual ℝ E) :
charFunDual μ L = charFun (Measure.map (⇑L) μ) 1
source
theorem MeasureTheory.charFun_map_eq_charFunDual_smul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [OpensMeasurableSpace E] (L : StrongDual ℝ E) (u : ℝ) :
charFun (Measure.map (⇑L) μ) u = charFunDual μ (u • L)
source
theorem MeasureTheory.charFun_eq_charFunDual_toDualMap {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} (t : E) :
charFun μ t = charFunDual μ ((InnerProductSpace.toDualMap ℝ E) t)
source
theorem MeasureTheory.charFunDual_map {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : Measure E} [OpensMeasurableSpace E] [BorelSpace F] (L : E →L[ℝ] F) (L' : StrongDual ℝ F) :
charFunDual (Measure.map (⇑L) μ) L' = charFunDual μ (ContinuousLinearMap.comp L' L)
source
@[simp]
theorem MeasureTheory.charFunDual_dirac {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {x : E} (L : StrongDual ℝ E) :
charFunDual (Measure.dirac x) L = Complex.exp (↑(L x) * Complex.I)
source
theorem MeasureTheory.charFunDual_map_add_const {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [BorelSpace E] (r : E) (L : StrongDual ℝ E) :
charFunDual (Measure.map (fun (x : E) => x + r) μ) L = charFunDual μ L * Complex.exp (↑(L r) * Complex.I)
source
theorem MeasureTheory.charFunDual_map_const_add {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [BorelSpace E] (r : E) (L : StrongDual ℝ E) :
charFunDual (Measure.map (fun (x : E) => r + x) μ) L = charFunDual μ L * Complex.exp (↑(L r) * Complex.I)
source
theorem MeasureTheory.charFunDual_prod {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : Measure E} {ν : Measure F} [SFinite μ] [SFinite ν] (L : StrongDual ℝ (E × F)) :
charFunDual (μ.prod ν) L = charFunDual μ (ContinuousLinearMap.comp L (ContinuousLinearMap.inl ℝ E F)) * charFunDual ν (ContinuousLinearMap.comp L (ContinuousLinearMap.inr ℝ E F))

The characteristic function of a product of measures is a product of characteristic functions. This is the version for Banach spaces, see `charFun_prod` for the Hilbert space version.

source
theorem MeasureTheory.charFunDual_prod' {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : Measure E} {ν : Measure F} (p : ENNReal) [Fact (1 ≤ p)] [SFinite μ] [SFinite ν] (L : StrongDual ℝ (WithLp p (E × F))) :
charFunDual (Measure.map (WithLp.toLp p) (μ.prod ν)) L = charFunDual μ (ContinuousLinearMap.comp L ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inl ℝ E F))) * charFunDual ν (ContinuousLinearMap.comp L ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inr ℝ E F)))

The characteristic function of a product of measures is a product of characteristic functions. This is `charFunDual_prod` for `WithLp`. See `charFun_prod` for the Hilbert space version.

source
theorem MeasureTheory.charFunDual_pi {ι : Type u_4} [Fintype ι] [DecidableEq ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → Measure (E i)} [∀ (i : ι), SigmaFinite (μ i)] (L : StrongDual ℝ ((i : ι) → E i)) :
charFunDual (Measure.pi μ) L = ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp L (ContinuousLinearMap.single ℝ E i))

The characteristic function of a product of measures is a product of characteristic functions. This is the version for Banach spaces, see `charFunDual_pi` for the Hilbert space version.

source
theorem MeasureTheory.charFunDual_pi' (p : ENNReal) [Fact (1 ≤ p)] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → Measure (E i)} [∀ (i : ι), SigmaFinite (μ i)] (L : StrongDual ℝ (PiLp p E)) :
charFunDual (Measure.map (WithLp.toLp p) (Measure.pi μ)) L = ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp L ((↑(PiLp.continuousLinearEquiv p ℝ E).symm).comp (ContinuousLinearMap.single ℝ E i)))

The characteristic function of a product of measures is a product of characteristic functions. This is `charFunDual_pi` for `PiLp`. See `charFunDual_pi` for the Banach space version.

source
theorem MeasureTheory.Measure.ext_of_charFunDual {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ ν : Measure E} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : charFunDual μ = charFunDual ν) :
μ = ν

If two finite measures have the same characteristic function, then they are equal.

source
theorem MeasureTheory.charFunDual_eq_prod_iff {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : Measure E} {ν : Measure F} [BorelSpace E] [SecondCountableTopology E] [BorelSpace F] [SecondCountableTopology F] [CompleteSpace E] [CompleteSpace F] {ξ : Measure (E × F)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteMeasure ξ] :
(∀ (L : StrongDual ℝ (E × F)), charFunDual ξ L = charFunDual μ (ContinuousLinearMap.comp L (ContinuousLinearMap.inl ℝ E F)) * charFunDual ν (ContinuousLinearMap.comp L (ContinuousLinearMap.inr ℝ E F))) ↔ ξ = μ.prod ν

The characteristic function of a measure is a product of characteristic functions if and only if it is a product measure. This is the version for Banach spaces, see `charFun_eq_prod_iff` for the Hilbert space version.

source
theorem MeasureTheory.charFunDual_eq_prod_iff' {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : Measure E} {ν : Measure F} [BorelSpace E] [SecondCountableTopology E] (p : ENNReal) [Fact (1 ≤ p)] [BorelSpace F] [SecondCountableTopology F] [CompleteSpace E] [CompleteSpace F] {ξ : Measure (E × F)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteMeasure ξ] :
(∀ (L : StrongDual ℝ (WithLp p (E × F))), charFunDual (Measure.map (WithLp.toLp p) ξ) L = charFunDual μ (ContinuousLinearMap.comp L ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inl ℝ E F))) * charFunDual ν (ContinuousLinearMap.comp L ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inr ℝ E F)))) ↔ ξ = μ.prod ν

The characteristic function of a measure is a product of characteristic functions if and only if it is a product measure. This is `charFunDual_eq_prod_iff` for `WithLp`. See `charFun_eq_prod_iff` for the Hilbert space version.

source
theorem MeasureTheory.charFunDual_eq_pi_iff {ι : Type u_4} [Fintype ι] [DecidableEq ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] [∀ (i : ι), CompleteSpace (E i)] {μ : (i : ι) → Measure (E i)} {ν : Measure ((i : ι) → E i)} [∀ (i : ι), IsFiniteMeasure (μ i)] [IsFiniteMeasure ν] :
(∀ (L : StrongDual ℝ ((i : ι) → E i)), charFunDual ν L = ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp L (ContinuousLinearMap.single ℝ E i))) ↔ ν = Measure.pi μ

The characteristic function of a measure is a product of characteristic functions if and only if it is a product measure. This is the version for Banach spaces, see `charFun_eq_pi_iff` for the Hilbert space version.

source
theorem MeasureTheory.charFunDual_eq_pi_iff' (p : ENNReal) [Fact (1 ≤ p)] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] [∀ (i : ι), CompleteSpace (E i)] {μ : (i : ι) → Measure (E i)} {ν : Measure ((i : ι) → E i)} [∀ (i : ι), IsFiniteMeasure (μ i)] [IsFiniteMeasure ν] :
(∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))), charFunDual (Measure.map (WithLp.toLp p) ν) L = ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp L ((↑(PiLp.continuousLinearEquiv p ℝ E).symm).comp (ContinuousLinearMap.single ℝ E i)))) ↔ ν = Measure.pi μ

The characteristic function of a measure is a product of characteristic functions if and only if it is a product measure. This is `charFunDual_eq_pi_iff` for `PiLp`. See `charFun_eq_pi_iff` for the Hilbert space version.

source
theorem MeasureTheory.charFunDual_conv {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [BorelSpace E] [SecondCountableTopology E] {μ ν : Measure E} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (L : StrongDual ℝ E) :
charFunDual (μ.conv ν) L = charFunDual μ L * charFunDual ν L

The characteristic function of a convolution of measures is the product of the respective characteristic functions.