MeasureTheory.Measure.dirac_apply_of_mem
theorem MeasureTheory.Measure.dirac_apply_of_mem :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α}, a ∈ s → ↑↑(MeasureTheory.Measure.dirac a) s = 1
This theorem states that for any type `α` with a `MeasurableSpace` instance and for any set `s` of type `α`, if an element `a` of type `α` belongs to the set `s`, then the dirac measure of `a` applied to the set `s` is equal to 1. The dirac measure is a function that assigns the value 1 to the set if `a` is in `s`, and 0 otherwise. The theorem essentially formalizes that when `a` belongs to the set `s`, the dirac measure of `a` on the set `s` is 1.
More concisely: For any measurable space `(α, Σ)` and set `s ∈ Σ` of type `α` with a `MeasurableSpace` instance, the Dirac measure of any `a ∈ s` evaluates to 1 on `s`.
|
MeasureTheory.Measure.sum_smul_dirac
theorem MeasureTheory.Measure.sum_smul_dirac :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Countable α] [inst_2 : MeasurableSingletonClass α]
(μ : MeasureTheory.Measure α), (MeasureTheory.Measure.sum fun a => ↑↑μ {a} • MeasureTheory.Measure.dirac a) = μ
The theorem `MeasureTheory.Measure.sum_smul_dirac` states that for any measure `μ` on a countable and measurable singleton type `α`, it can be represented as a sum of Dirac measures, each scaled by the measure of the corresponding singleton set. In other words, any measure in such a set-up can be broken down into a series of "point masses" (Dirac measures), each located at a unique point in the space and weighed by the measure of that point. This is an important theorem in measure theory because it demonstrates that the concept of a measure can be generalized from simple summation of values at points (as in Dirac measures) to more complex structures that account for densities and distributions.
More concisely: For any countable and measurable singleton type in a measure space, the measure can be represented as a sum of Dirac measures, each scaled by the measure of the corresponding singleton set.
|
MeasureTheory.Measure.map_eq_sum
theorem MeasureTheory.Measure.map_eq_sum :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : Countable β]
[inst_3 : MeasurableSingletonClass β] (μ : MeasureTheory.Measure α) (f : α → β),
Measurable f →
MeasureTheory.Measure.map f μ =
MeasureTheory.Measure.sum fun b => ↑↑μ (f ⁻¹' {b}) • MeasureTheory.Measure.dirac b
The theorem `MeasureTheory.Measure.map_eq_sum` states that if `f` is a measurable function from a measurable space `α` to another measurable space `β` with a countable number of elements, then the pushforward measure of `μ` under `f` is equal to the sum of Dirac measures. Each Dirac measure in the sum is scaled by the measure of the preimage under `f` of each singleton set in `β`. In mathematical terms, this is saying that if `f: α → β` is measurable and `β` is countable, then the pushforward of a measure `μ` under `f` is the sum over `b` in `β` of the measure of the preimage of `{b}` times the Dirac measure at `b`.
More concisely: If `μ` is a measure on a measurable space `α`, `f: α → β` is a countable measurable function to a measurable space `β`, then the pushforward measure of `μ` under `f` equals the sum of scaled Dirac measures, where the scale is the measure of `f`'s preimage of each singleton set in `β`.
|
MeasureTheory.Measure.dirac_apply'
theorem MeasureTheory.Measure.dirac_apply' :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} (a : α),
MeasurableSet s → ↑↑(MeasureTheory.Measure.dirac a) s = s.indicator 1 a
This theorem states that for any measurable space `α`, any set `s` of type `α`, and any element `a` of type `α`, if `s` is a measurable set, then the measure of set `s` under the Dirac measure centered at `a` is equal to the indicator function of set `s` evaluated at `a` with the function mapping each element to one. In simpler terms, if we have a set `s` in a measurable space, the Dirac measure of `s` at a point `a` is 1 if `a` is in the set `s` and 0 otherwise.
More concisely: For any measurable space `α`, any measurable set `s` of type `α`, and any point `a` in `α`, the Dirac measure of `s` at `a` equals the indicator function of `s` evaluated at `a`.
|
MeasureTheory.Measure.restrict_singleton
theorem MeasureTheory.Measure.restrict_singleton :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (a : α),
μ.restrict {a} = ↑↑μ {a} • MeasureTheory.Measure.dirac a
This theorem states that for any type `α` with a measurable space structure, any measure `μ` on `α`, and any element `a` of `α`, the restriction of `μ` to the singleton set `{a}` is equal to `{a}` under `μ` times the Dirac measure at `a`. In other words, when we restrict a measure to a single point, it behaves just like the Dirac measure at that point, scaled by the measure of the point under the original measure.
More concisely: For any measurable space `(α, Σ)`, measure `μ`, and `Σ-`measurable `a ∈ α`, the restriction of `μ` to the singleton set `{a}` is equal to the Dirac measure `δ_a` multiplied by the measure `μ({a})`. In Lean notation, `μ {a} = δ_a ⊤ (μ ∘ iCarrier a)`.
|
MeasureTheory.Measure.tsum_indicator_apply_singleton
theorem MeasureTheory.Measure.tsum_indicator_apply_singleton :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Countable α] [inst_2 : MeasurableSingletonClass α]
(μ : MeasureTheory.Measure α) (s : Set α),
MeasurableSet s → ∑' (x : α), s.indicator (fun x => ↑↑μ {x}) x = ↑↑μ s
The theorem, `MeasureTheory.Measure.tsum_indicator_apply_singleton`, states that for any given countable, measurable space `α`, where all singleton sets are measurable, the measure of a set `s` under a measure `μ` can be expressed as the sum (or infinite series) of the measure of each singleton set `{x}` for all `x` belonging to `s`. This is, the measure of `s` is equal to the sum over all `α` of the indicator function of `s` applied to `x` times the measure of `{x}`. The indicator function is 1 for elements in the set `s` and 0 otherwise. This essentially breaks down the measure of a set into the measures of its individual elements.
More concisely: For any countable measurable space `(α, Σ, μ)` where all singletons are measurable, the measure of a set `s ∈ Σ` is equal to the sum of the measures of its singleton elements `{x} ∈ s`, i.e., μ(s) = Σₓ∈s μ({x}).
|
MeasureTheory.Measure.dirac_apply
theorem MeasureTheory.Measure.dirac_apply :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (a : α) (s : Set α),
↑↑(MeasureTheory.Measure.dirac a) s = s.indicator 1 a
The theorem `MeasureTheory.Measure.dirac_apply` states that for any type `α` that has a measurable space structure and a measurable singleton class structure, any element `a` of type `α`, and any set `s` of elements of type `α`, the measure of the set `s` under the dirac measure centered at `a` is equal to the indicator function of `s` evaluated at `a`. This indicator function is defined such that it equals 1 if `a` belongs to `s`, and 0 otherwise. In other words, the dirac measure of a set `s` at a point `a` is 1 if `a` is in `s`, and 0 otherwise.
More concisely: For any measurable space and measurable singleton class structure on type `α`, the dirac measure of a set `s` at point `a` equals the indicator function of `s` evaluated at `a`.
|
MeasureTheory.Measure.map_dirac
theorem MeasureTheory.Measure.map_dirac :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
Measurable f →
∀ (a : α), MeasureTheory.Measure.map f (MeasureTheory.Measure.dirac a) = MeasureTheory.Measure.dirac (f a)
This theorem, `MeasureTheory.Measure.map_dirac`, states that for two types `α` and `β` each equipped with a measurable space structure, and a function `f` from `α` to `β` which is measurable, the pushforward of the Dirac measure at any point `a` of type `α` under the function `f` is equivalent to the Dirac measure at `f(a)`. In other words, in the context of measure theory, mapping the Dirac measure at a point `a` through a measurable function `f` effectively shifts the "location" of the Dirac measure from `a` to `f(a)`.
More concisely: For measurable spaces `(α, Σα)` and `(β, Σβ)`, measurable function `f : α → β`, and `a ∈ α`, the pushforward of the Dirac measure at `a` under `f` equals the Dirac measure at `f(a)`.
|
MeasureTheory.ae_dirac_eq
theorem MeasureTheory.ae_dirac_eq :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (a : α),
(MeasureTheory.Measure.dirac a).ae = pure a
The theorem `MeasureTheory.ae_dirac_eq` states that for any measurable space `α` and any element `a` of `α`, the "almost everywhere" filter of co-null sets corresponding to the Dirac measure at `a` is equivalent to the filter which contains exactly the set `{a}`. This essentially means that the Dirac measure at `a` is zero almost everywhere except at the point `a` itself. This applies to any measurable singleton class, which is a class of measurable spaces where every singleton set `{a}` is measurable.
More concisely: The almost everywhere filter of co-null sets for the Dirac measure at a point in a measurable space is equivalent to the filter generated by the singleton set containing that point.
|