Elementary theory of the Cauchy law

This file develops the elementary transform theory of Mathlib's Cauchy law. For nonzero scale γ the cumulative distribution function at x is

1 / 2 + arctan ((x - x₀) / γ) / π,

and for every scale, including the degenerate one, the characteristic function is

t ↦ exp (t x₀ i - γ |t|).

The nondegenerate law has no first absolute moment, and its exponential integrand is integrable only at rate zero. These statements record the sharp heavy-tail behavior that distinguishes the Cauchy family from the light-tailed distributions developed alongside it.

At scale zero Mathlib defines cauchyMeasure x₀ 0 to be the Dirac mass at x₀. The file records the corresponding cumulative distribution function, mean, variance, exponential-integrability domain, moment-generating function, and cumulant-generating function. Keeping the singular case separate prevents the density calculation for positive scale from being applied where the law is not absolutely continuous; the characteristic function, by contrast, is a single formula covering both cases.

The characteristic function is obtained from the Fourier inversion theorem applied to TauCeti.fourier_exp_neg_mul_abs: the Fourier transform of the two-sided exponential of rate 2 π γ is the centred Cauchy density of scale γ, so inverting it pairs that density against exp (i t x) and returns the two-sided exponential again. The exponent in the resulting formula is linear in x₀ and γ, so products of characteristic functions add the locations and scales. Hence convolving Cauchy laws adds their parameters, and scaling a sum of n independent copies by 1 / n restores the original parameters. Thus the sample mean of independent Cauchy variables with a common location and scale has exactly the parent law.

Main results

• TauCeti.Probability.hasDerivAt_arctan_div_pi — the derivative underlying the cdf formula;
• TauCeti.Probability.integral_Iic_cauchyPDFReal — the integral of the Cauchy density over a left half-line;
• TauCeti.Probability.cdf_cauchyMeasure_of_scale_ne_zero — the Cauchy cdf at nonzero scale;
• TauCeti.Probability.cdf_cauchyMeasure_zero_scale — the cdf of the zero-scale Dirac law;
• TauCeti.Probability.not_integrable_id_cauchyMeasure — a nondegenerate Cauchy law has no first moment;
• TauCeti.Probability.integrableExpSet_id_cauchyMeasure — its exponential-integrability domain is {0};
• TauCeti.Probability.integrable_exp_mul_id_cauchyMeasure_iff — an exponential integrand is integrable exactly when its scale or rate is zero;
• TauCeti.Probability.integral_id_cauchyMeasure_zero_scale and TauCeti.Probability.variance_id_cauchyMeasure_zero_scale — the zero-scale mean and variance;
• TauCeti.Probability.integrableExpSet_id_cauchyMeasure_zero_scale, TauCeti.Probability.mgf_id_cauchyMeasure_zero_scale, and TauCeti.Probability.cgf_id_cauchyMeasure_zero_scale — the zero-scale exponential moments;
• TauCeti.Probability.cauchyPDFReal_zero_loc_isBigO_rpow_neg_two — centred Cauchy density has quadratic decay at infinity;
• TauCeti.Probability.contDiff_cauchyPDFReal — the Cauchy density is smooth;
• TauCeti.Probability.fourier_exp_neg_mul_abs_eq_cauchyPDFReal_zero_loc and TauCeti.Probability.integral_exp_mul_I_mul_cauchyPDFReal_zero_loc — the Fourier pair behind the transform;
• TauCeti.Probability.cauchyMeasure_map_add_const — translation changes the location parameter;
• TauCeti.Probability.charFun_cauchyMeasure — the characteristic function of cauchyMeasure x₀ γ;
• TauCeti.Probability.cauchyMeasure_conv_cauchyMeasure — convolution adds locations and scales;
• ProbabilityTheory.IndepFun.hasLaw_add_cauchyMeasure — the same for sums of independent Cauchy variables;
• ProbabilityTheory.iIndepFun.hasLaw_average_cauchyMeasure — stability of the family under averaging.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, 2nd ed., Wiley, 1994.

Provenance

The centred-density quadratic decay estimate is adapted from the Cauchy-lattice Poisson development in the [AIQ-Kitware DKPS formalization] (https://github.com/AIQ-Kitware/aiq-dkps-formalization), Apache-2.0; Jon Crall and GPT 5.6 High.

theorem TauCeti.Probability.cauchyPDFReal_zero_loc_isBigO_rpow_neg_two (γ : NNReal) : (fun (x : ℝ) => ProbabilityTheory.cauchyPDFReal 0 γ x) =O[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ (-2)

The centred Cauchy density is O(|x|⁻²) at infinity, including zero scale.

theorem TauCeti.Probability.contDiff_cauchyPDFReal (x₀ : ℝ) (γ : NNReal) {n : WithTop ℕ∞} : ContDiff ℝ n (ProbabilityTheory.cauchyPDFReal x₀ γ)

The Cauchy density is smooth, including at zero scale, where it vanishes identically.

theorem TauCeti.Probability.hasDerivAt_arctan_div_pi (x₀ : ℝ) (γ : NNReal) (y : ℝ) : HasDerivAt (fun (z : ℝ) => Real.arctan ((z - x₀) / ↑γ) / Real.pi) (ProbabilityTheory.cauchyPDFReal x₀ γ y) y

The scaled arctangent has the Cauchy density as its derivative.

theorem TauCeti.Probability.integral_Iic_cauchyPDFReal (x₀ : ℝ) {γ : NNReal} (hγ : γ ≠ 0) (x : ℝ) : ∫ (y : ℝ) in Set.Iic x, ProbabilityTheory.cauchyPDFReal x₀ γ y = 1 / 2 + Real.arctan ((x - x₀) / ↑γ) / Real.pi

The integral of a nondegenerate Cauchy density over a left half-line is given by the scaled arctangent.

@[simp]

theorem TauCeti.Probability.cdf_cauchyMeasure_of_scale_ne_zero (x₀ : ℝ) {γ : NNReal} (hγ : γ ≠ 0) (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.cauchyMeasure x₀ γ)) x = 1 / 2 + Real.arctan ((x - x₀) / ↑γ) / Real.pi

The cumulative distribution function of a nondegenerate Cauchy law.

theorem TauCeti.Probability.cdf_cauchyMeasure_zero_scale (x₀ x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.cauchyMeasure x₀ 0)) x = if x₀ ≤ x then 1 else 0

The cumulative distribution function at zero scale. Mathlib totalizes the Cauchy family by setting cauchyMeasure x₀ 0 = Measure.dirac x₀.

theorem TauCeti.Probability.integral_id_cauchyMeasure_zero_scale (x₀ : ℝ) : ∫ (x : ℝ), x ∂ProbabilityTheory.cauchyMeasure x₀ 0 = x₀

The mean of the zero-scale Cauchy law is its location.

theorem TauCeti.Probability.variance_id_cauchyMeasure_zero_scale (x₀ : ℝ) : ProbabilityTheory.variance id (ProbabilityTheory.cauchyMeasure x₀ 0) = 0

The zero-scale Cauchy law has zero variance.

theorem TauCeti.Probability.integrableExpSet_id_cauchyMeasure_zero_scale (x₀ : ℝ) : ProbabilityTheory.integrableExpSet id (ProbabilityTheory.cauchyMeasure x₀ 0) = Set.univ

Every exponential moment of the zero-scale Cauchy law exists.

theorem TauCeti.Probability.mgf_id_cauchyMeasure_zero_scale (x₀ t : ℝ) : ProbabilityTheory.mgf id (ProbabilityTheory.cauchyMeasure x₀ 0) t = Real.exp (t * x₀)

The moment-generating function of the zero-scale Cauchy law.

theorem TauCeti.Probability.cgf_id_cauchyMeasure_zero_scale (x₀ t : ℝ) : ProbabilityTheory.cgf id (ProbabilityTheory.cauchyMeasure x₀ 0) t = t * x₀

The cumulant-generating function of the zero-scale Cauchy law.

theorem TauCeti.Probability.integrable_cauchyMeasure_iff {γ : NNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ : ℝ) (hγ : γ ≠ 0) {g : ℝ → E} : MeasureTheory.Integrable g (ProbabilityTheory.cauchyMeasure x₀ γ) ↔ MeasureTheory.Integrable (fun (x : ℝ) => ProbabilityTheory.cauchyPDFReal x₀ γ x • g x) MeasureTheory.volume

Integrability transfer at nonzero scale. A function is integrable against a nondegenerate Cauchy law exactly when its density-weighted version is Lebesgue integrable.

theorem TauCeti.Probability.integral_cauchyMeasure_eq {γ : NNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ : ℝ) (hγ : γ ≠ 0) (g : ℝ → E) : ∫ (x : ℝ), g x ∂ProbabilityTheory.cauchyMeasure x₀ γ = ∫ (x : ℝ), ProbabilityTheory.cauchyPDFReal x₀ γ x • g x

Integral transfer at nonzero scale. An integral against a nondegenerate Cauchy law is the density-weighted Lebesgue integral.

theorem TauCeti.Probability.not_integrable_id_cauchyMeasure {γ : NNReal} (x₀ : ℝ) (hγ : γ ≠ 0) : ¬MeasureTheory.Integrable id (ProbabilityTheory.cauchyMeasure x₀ γ)

A nondegenerate Cauchy law has no first absolute moment.

theorem TauCeti.Probability.not_integrable_exp_mul_id_cauchyMeasure {γ : NNReal} (x₀ : ℝ) (hγ : γ ≠ 0) {t : ℝ} (ht : t ≠ 0) : ¬MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (ProbabilityTheory.cauchyMeasure x₀ γ)

The exponential of a nonzero multiple of the identity is not integrable under a nondegenerate Cauchy law.

@[simp]

theorem TauCeti.Probability.integrable_exp_mul_id_cauchyMeasure_iff (x₀ : ℝ) (γ : NNReal) (t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (ProbabilityTheory.cauchyMeasure x₀ γ) ↔ γ = 0 ∨ t = 0

The exponential integrand of a Cauchy law is integrable exactly when the scale or rate is zero.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_cauchyMeasure {γ : NNReal} (x₀ : ℝ) (hγ : γ ≠ 0) : ProbabilityTheory.integrableExpSet id (ProbabilityTheory.cauchyMeasure x₀ γ) = {0}

The exponential-integrability domain of a nondegenerate Cauchy law is the singleton {0}.

@[simp]

theorem TauCeti.Probability.cauchyMeasure_map_add_const (x₀ y : ℝ) (γ : NNReal) : MeasureTheory.Measure.map (fun (x : ℝ) => x + y) (ProbabilityTheory.cauchyMeasure x₀ γ) = ProbabilityTheory.cauchyMeasure (x₀ + y) γ

Translating a Cauchy distribution changes its location parameter by the same amount.

theorem TauCeti.Probability.fourier_exp_neg_mul_abs_eq_cauchyPDFReal_zero_loc {γ : NNReal} (hγ : γ ≠ 0) (ξ : ℝ) : FourierTransform.fourier (fun (x : ℝ) => ↑(Real.exp (-(2 * Real.pi * ↑γ * |x|)))) ξ = ↑(ProbabilityTheory.cauchyPDFReal 0 γ ξ)

The Fourier transform of the two-sided exponential of rate 2 π γ is the Cauchy density of scale γ centred at the origin. This is TauCeti.fourier_exp_neg_mul_abs at the rate that makes the Lorentzian a probability density.

theorem TauCeti.Probability.integral_exp_mul_I_mul_cauchyPDFReal_zero_loc {γ : NNReal} (hγ : γ ≠ 0) (t : ℝ) : ∫ (x : ℝ), Complex.exp (↑t * ↑x * Complex.I) * ↑(ProbabilityTheory.cauchyPDFReal 0 γ x) = ↑(Real.exp (-(↑γ * |t|)))

The oscillatory integral of the centred Cauchy density. Pairing the Cauchy density of scale γ against exp (i t x) returns the two-sided exponential exp (-(γ * |t|)).

@[simp]

theorem TauCeti.Probability.charFun_cauchyMeasure (x₀ : ℝ) (γ : NNReal) (t : ℝ) : MeasureTheory.charFun (ProbabilityTheory.cauchyMeasure x₀ γ) t = Complex.exp (↑t * ↑x₀ * Complex.I - ↑↑γ * ↑|t|)

The characteristic function of the Cauchy distribution. For location x₀ and scale γ it is t ↦ exp (t x₀ i - γ |t|). The formula is uniform in the scale: at γ = 0 Mathlib's cauchyMeasure x₀ 0 is the Dirac mass at x₀, whose characteristic function is t ↦ exp (t x₀ i).

theorem TauCeti.Probability.cauchyMeasure_conv_cauchyMeasure (x₁ x₂ : ℝ) (γ₁ γ₂ : NNReal) : (ProbabilityTheory.cauchyMeasure x₁ γ₁).conv (ProbabilityTheory.cauchyMeasure x₂ γ₂) = ProbabilityTheory.cauchyMeasure (x₁ + x₂) (γ₁ + γ₂)

The Cauchy family is closed under convolution. Convolving two Cauchy laws adds their locations and their scales, including the zero-scale Dirac laws.

theorem ProbabilityTheory.iIndepFun.hasLaw_average_cauchyMeasure {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {x₀ : ℝ} {γ : NNReal} {X : ι → Ω → ℝ} (hindep : iIndepFun X P) (hlaw : ∀ (i : ι), HasLaw (X i) (cauchyMeasure x₀ γ) P) : HasLaw (fun (ω : Ω) => (↑(Fintype.card ι))⁻¹ * ∑ i : ι, X i ω) (cauchyMeasure x₀ γ) P

The Cauchy family is stable under averaging. The sample mean of a nonempty finite family of independent Cauchy variables with common location x₀ and scale γ has exactly the same law.

theorem ProbabilityTheory.IndepFun.hasLaw_add_cauchyMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {x₁ x₂ : ℝ} {γ₁ γ₂ : NNReal} (hXY : IndepFun X Y P) (hX : HasLaw X (cauchyMeasure x₁ γ₁) P) (hY : HasLaw Y (cauchyMeasure x₂ γ₂) P) : HasLaw (X + Y) (cauchyMeasure (x₁ + x₂) (γ₁ + γ₂)) P

The sum of independent Cauchy variables is Cauchy, with the locations and the scales added.