Documentation

TauCeti.Probability.Distributions.Semicircle.PDF

Density of the semicircle law #

The unit-radius semicircle law has the continuous density 2 / π * √(1 - x²). The real square root makes this expression zero outside the open interval (-1, 1), in particular at the endpoints ±1. The affine Beta realization gives the density-measure equality and the random-variable and Radon–Nikodym interfaces, and expresses integration against the law as an interval integral against the semicircle height.

References #

source
noncomputable def TauCeti.Probability.semicirclePDFReal (x : ℝ) :
ℝ

The real density of the unit-radius semicircle law, zero outside (-1, 1).

Instances For
    source
    noncomputable def TauCeti.Probability.semicirclePDF (x : ℝ) :
    ENNReal

    The extended nonnegative density of the unit-radius semicircle law.

    Instances For
      source
      theorem TauCeti.Probability.semicirclePDFReal_apply (x : ℝ) :
      semicirclePDFReal x = 2 / Real.pi * √(1 - x ^ 2)

      The semicircle density is the scaled height of the unit semicircle.

      source
      @[simp]
      theorem TauCeti.Probability.semicirclePDF_apply (x : ℝ) :
      semicirclePDF x = ENNReal.ofReal (semicirclePDFReal x)

      The extended density is obtained from the real density by ENNReal.ofReal.

      source
      theorem TauCeti.Probability.semicirclePDFReal_nonneg (x : ℝ) :
      0 ≤ semicirclePDFReal x

      The semicircle density is nonnegative.

      source
      @[simp]
      theorem TauCeti.Probability.semicirclePDFReal_pos_iff {x : ℝ} :
      0 < semicirclePDFReal x ↔ x ∈ Set.Ioo (-1) 1

      The density is positive exactly in the interior of the support.

      source
      theorem TauCeti.Probability.continuous_semicirclePDFReal :
      Continuous semicirclePDFReal

      The real density is continuous, including at the support endpoints.

      source
      theorem TauCeti.Probability.measurable_semicirclePDF :
      Measurable semicirclePDF

      The extended density is measurable.

      source
      theorem TauCeti.Probability.semicircleMeasure_eq_withDensity :
      semicircleMeasure = MeasureTheory.volume.withDensity semicirclePDF

      The semicircle law is Lebesgue measure weighted by its named density.

      source
      theorem TauCeti.Probability.integral_semicircleMeasure_eq_intervalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) :
      ∫ (x : ℝ), f x ∂semicircleMeasure = (2 / Real.pi) • ∫ (x : ℝ) in -1..1, √(1 - x ^ 2) • f x

      Integration against the unit-radius semicircle law, as an interval integral against the semicircle height.

      source
      @[simp]
      theorem TauCeti.Probability.map_neg_semicircleMeasure :
      MeasureTheory.Measure.map Neg.neg semicircleMeasure = semicircleMeasure

      Reflection preserves the unit-radius semicircle law.

      source
      instance TauCeti.Probability.nullSingletonClass_semicircleMeasure :
      MeasureTheory.NullSingletonClass semicircleMeasure

      The semicircle law has no atoms.

      source
      theorem TauCeti.Probability.hasPDF_of_hasLaw_semicircleMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X semicircleMeasure P) :
      MeasureTheory.HasPDF X P MeasureTheory.volume

      A variable with semicircle law has a density.

      source
      theorem TauCeti.Probability.pdf_eq_semicirclePDF_of_hasLaw_semicircleMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X semicircleMeasure P) :
      MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] semicirclePDF

      The density of a variable with semicircle law agrees almost everywhere with its named pdf.

      source
      theorem TauCeti.Probability.rnDeriv_semicircleMeasure :
      semicircleMeasure.rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] semicirclePDF

      The Radon–Nikodym derivative of the semicircle law is its named pdf.