Cauchy Distribution over ℝ

Define the Cauchy distribution with location parameter x₀ and scale parameter γ.

Note that we use "location" and "scale" to refer to these parameters in theorem names.

Main definition

• cauchyPDFReal: the function x₀ γ x ↦ π⁻¹ * γ * ((x - x₀) ^ 2 + γ ^ 2)⁻¹, which is the probability density function of a Cauchy distribution with location parameter x₀ and scale parameter γ (when γ ≠ 0).
• cauchyPDF: ℝ≥0∞-valued pdf, cauchyPDF μ v x = ENNReal.ofReal (cauchyPDFReal μ v x).
• cauchyMeasure: a Cauchy measure on ℝ, parametrized by a location parameter x₀ : ℝ and a scale parameter γ : ℝ≥0. If γ = 0, this is dirac x₀, otherwise it is defined as the measure with density cauchyPDF x₀ γ with respect to the Lebesgue measure.

noncomputable def ProbabilityTheory.cauchyPDFReal (x₀ : ℝ) (γ : NNReal) (x : ℝ) : ℝ

The pdf of the cauchy distribution depending on its location x₀ and scale γ parameters.

@[simp]

theorem ProbabilityTheory.cauchyPDFReal_scale_zero (x₀ : ℝ) : cauchyPDFReal x₀ 0 = 0

theorem ProbabilityTheory.cauchyPDFReal_def (x₀ : ℝ) (γ : NNReal) (x : ℝ) : cauchyPDFReal x₀ γ x = Real.pi⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹

theorem ProbabilityTheory.cauchyPDFReal_def' (x₀ : ℝ) (γ : NNReal) (x : ℝ) : cauchyPDFReal x₀ γ x = Real.pi⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹

noncomputable def ProbabilityTheory.cauchyPDF (x₀ : ℝ) (γ : NNReal) (x : ℝ) : ENNReal

The pdf of the gamma distribution, as a function valued in ℝ≥0∞.

@[simp]

theorem ProbabilityTheory.cauchyPDF_scale_zero (x₀ : ℝ) : cauchyPDF x₀ 0 = 0

theorem ProbabilityTheory.cauchyPDF_def (x₀ : ℝ) (γ : NNReal) (x : ℝ) : cauchyPDF x₀ γ x = ENNReal.ofReal (cauchyPDFReal x₀ γ x)

theorem ProbabilityTheory.measurable_cauchyPDFReal (x₀ : ℝ) (γ : NNReal) : Measurable (cauchyPDFReal x₀ γ)

theorem ProbabilityTheory.stronglyMeasurable_cauchyPDFReal (x₀ : ℝ) (γ : NNReal) : MeasureTheory.StronglyMeasurable (cauchyPDFReal x₀ γ)

theorem ProbabilityTheory.measurable_cauchyPDF (x₀ : ℝ) (γ : NNReal) : Measurable (cauchyPDF x₀ γ)

theorem ProbabilityTheory.stronglyMeasurable_cauchyPDF (x₀ : ℝ) (γ : NNReal) : MeasureTheory.StronglyMeasurable (cauchyPDF x₀ γ)

theorem ProbabilityTheory.cauchyPDF_pos (x₀ : ℝ) {γ : NNReal} (hγ : γ ≠ 0) (x : ℝ) : 0 < cauchyPDFReal x₀ γ x

cauchyPDFReal is positive for γ > 0.

theorem ProbabilityTheory.integral_cauchyPDFReal_eq_one (x₀ : ℝ) {γ : NNReal} (hγ : γ ≠ 0) : ∫ (x : ℝ), cauchyPDFReal x₀ γ x = 1

theorem ProbabilityTheory.integrable_cauchyPDFReal (x₀ : ℝ) {γ : NNReal} : MeasureTheory.Integrable (cauchyPDFReal x₀ γ) MeasureTheory.volume

@[simp]

theorem ProbabilityTheory.lintegral_cauchyPDF_eq_one (x₀ : ℝ) {γ : NNReal} (hγ : γ ≠ 0) : ∫⁻ (x : ℝ), cauchyPDF x₀ γ x = 1

The pdf of the cauchy distribution integrates to 1.

noncomputable def ProbabilityTheory.cauchyMeasure (x₀ : ℝ) (γ : NNReal) : MeasureTheory.Measure ℝ

A Cauchy distribution on ℝ with location parameter x₀ and scale parameter γ.

theorem ProbabilityTheory.cauchyMeasure_of_scale_ne_zero (x₀ : ℝ) {γ : NNReal} (hγ : γ ≠ 0) : cauchyMeasure x₀ γ = MeasureTheory.volume.withDensity (cauchyPDF x₀ γ)

@[simp]

theorem ProbabilityTheory.cauchyMeasure_zero_scale (x₀ : ℝ) : cauchyMeasure x₀ 0 = MeasureTheory.Measure.dirac x₀

instance ProbabilityTheory.instIsProbabilityMeasure_cauchyMeasure (x₀ : ℝ) (γ : NNReal) : MeasureTheory.IsProbabilityMeasure (cauchyMeasure x₀ γ)