How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A Dirac set function is a probability measure
Statement
For , the Dirac set function is a probability measure on every sigma-algebra on .
Facts & Assumptions
Given: A sigma-algebra on a nonempty set and a point .
The Dirac set function has value exactly on the measurable sets containing , and value otherwise (The Dirac set function at a point).
A probability measure is a measure whose value on the whole space is (Probability measures and probability spaces).
A nonnegative extended series is the supremum of its finite partial sums, with the empty sum equal to (Series in the nonnegative extended real line).
Proof
One has and .
If is pairwise disjoint, then belongs to at most one . If it belongs to none, both and are ; if it belongs to the unique , both are .
Step 1.2 proves countable additivity and step 1.1 gives the empty-set and total-mass conditions, so is a probability measure.
Depends on
Used by
- Higher-dimensional simple symmetric walks are transient Corollary
- One-dimensional simple symmetric walk is recurrent Corollary
- Two-dimensional simple symmetric walk is recurrent Corollary
- A submartingale need not have increasing sample paths Counterexample
- An adapted process need not be a martingale Counterexample
- An unbounded predictable transform may lose integrability Counterexample
- Doubling ergodicity depends on the invariant measure Counterexample
- Equal finitely many moments do not determine a law Counterexample
- Taking out an unbounded factor needs integrability Counterexample
- Complex Lp classes and Euclidean test-function conventions Definition
- A boundary atom gives an h1 function without an L1 density Example
- A Dirac probability measure concentrates all mass at one point Example
- A singular inner function generated by a point mass Example
- A step function generates a finite atomic measure Example
- Assuming choice, the completion of the Borel Dirac measure at zero is defined on every subset of the real line Example
- Birth–death recurrence through scale products Example
- Borel-Cantelli for the shrinking intervals (0,2⁻ᵏ) under a dyadic atomic measure Example
- Characteristic functions of bernoulli binomial and poisson laws Example
- Chebyshev extremal nodes converge to the arcsine equilibrium measure Example
- Extreme points of the probability measures are Dirac masses Example
- Gambler’s ruin from harmonicity Example
- Green kernel of a biased integer walk Example
- Independent sums via characteristic functions Example
- Integrating against a Dirac measure is evaluation at the point Example
- Point evaluation is represented by a Dirac measure Example
- Square of a martingale minus quadratic compensator Example
- The measure δ₀+λ↾_[0,1] splits into discrete and absolutely continuous parts Example
- The weights 2⁻⁽ᵏ⁺¹⁾ define a probability measure on P(ℕ) Example
- False: constant continuous invariants characterize measure ergodicity False statement
- FALSE: measures are additive on arbitrary countable unions False statement
- Monic polynomial lower bounds for the Chebyshev constant and capacity Lemma
- A measure on a finite sigma-algebra is a finite weighted sum over its atoms Theorem
- Every finite Borel measure on ℝ splits as an atomic part plus an atomless part Theorem
- Every measure on a countable discrete space is its weighted sum of Dirac measures Theorem
- Fekete–Szegő equality of logarithmic capacity, transfinite diameter, and Chebyshev constant Theorem
- h1 is isometric to finite regular complex boundary measures Theorem
- Krylov–Bogolyubov existence of an invariant probability Theorem
- Lyapunov drift bound for hitting times Theorem
- Recurrence and transience are class properties Theorem
Cited to discharge well-definedness by The Dirac set function at a point.
Dependency tree · two levels
9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- T. Tao, An Introduction to Measure Theory, Example 1.4.29 (standard reference, not scraped)