noncomputable def measureConv (μ ν : MeasureTheory.Measure ℝ) : MeasureTheory.Measure ℝ

Convolution of two measures on ℝ: the pushforward of the product measure μ.prod ν under the addition map (x, y) ↦ x + y.

def convPow (ν : MeasureTheory.Measure ℝ) : ℕ → MeasureTheory.Measure ℝ

The n-fold convolution power of a measure ν on ℝ. By convention convPow ν 0 is the Dirac mass at 0 and convPow ν (n+1) = (convPow ν n) ∗ ν.

def ProbabilityTheory.IsSlowlyVarying (L : ℝ → ℝ) : Prop

L : ℝ → ℝ is slowly varying (at infinity) if it is positive on (0, ∞) and L(cx) / L(x) → 1 as x → ∞ for every c > 0.

def ProbabilityTheory.IsRegularlyVarying (f : ℝ → ℝ) (ρ : ℝ) : Prop

f is regularly varying with index ρ if it can be written as f x = x^ρ · L x eventually as x → ∞, where L is slowly varying.

def ProbabilityTheory.rightTail (μ : MeasureTheory.Measure ℝ) (x : ℝ) : ℝ

The right tail probability μ((x, ∞)) as a real number.

def ProbabilityTheory.leftTail (μ : MeasureTheory.Measure ℝ) (x : ℝ) : ℝ

The left tail probability μ((-∞, -x]) as a real number.

def ProbabilityTheory.combinedTail (μ : MeasureTheory.Measure ℝ) (x : ℝ) : ℝ

The two-sided tail μ(|X| > x) written as the sum of the right and left tails.

def ProbabilityTheory.IsStable (μ : MeasureTheory.Measure ℝ) (α : ℝ) : Prop

A probability measure μ on ℝ is stable with index α ∈ (0, 2] if for every n > 0 there exist constants aₙ > 0 and bₙ such that the n-fold convolution μ * μ * ⋯ * μ equals the pushforward of μ under the affine map x ↦ aₙ x + bₙ.

def ProbabilityTheory.IsNondegenerate (μ : MeasureTheory.Measure ℝ) : Prop

A measure μ on ℝ is nondegenerate if it is not a point mass δ_a for any a.

def ProbabilityTheory.InDomainOfAttraction (μ G : MeasureTheory.Measure ℝ) : Prop

The probability measure μ is in the domain of attraction of G if there exist sequences of normalizing constants a n > 0 and centering constants b n such that the law of (S_n - b n) / a n (where S_n has law μ^{*n}) converges weakly to G, expressed here as integration against arbitrary bounded continuous functions.

def ProbabilityTheory.HasTailBalance (μ : MeasureTheory.Measure ℝ) (p : ℝ) : Prop

μ has tail balance with parameter p ∈ [0, 1] if the ratio of the right tail to the combined two-sided tail tends to p as x → ∞, i.e. P(X > x) / P(|X| > x) → p.

theorem ProbabilityTheory.domain_of_attraction_limit_is_stable (μ G : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure G] (hG : IsNondegenerate G) (hDA : InDomainOfAttraction μ G) : ∃ (α : ℝ), IsStable G α

If μ lies in the domain of attraction of a nondegenerate probability measure G, then G must be a stable law (with some index α ∈ (0, 2]).

def ProbabilityTheory.InDomainOfAttractionIndex (μ : MeasureTheory.Measure ℝ) (α : ℝ) : Prop

μ is in the domain of attraction of index α if there exists a stable law G of index α such that μ is in the domain of attraction of G.

theorem ProbabilityTheory.domain_of_attraction_of_tail_conditions (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (α : ℝ) (hα₁ : 0 < α) (hα₂ : α < 2) (hRV : IsRegularlyVarying (combinedTail μ) (-α)) (hTB : ∃ (p : ℝ), HasTailBalance μ p) : InDomainOfAttractionIndex μ α

For α ∈ (0, 2), the tail conditions (regular variation of index -α for the combined tail and existence of a tail balance parameter) are sufficient for μ to lie in the domain of attraction of a stable law of index α.

theorem ProbabilityTheory.tail_conditions_of_domain_of_attraction (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (α : ℝ) (hα₁ : 0 < α) (hα₂ : α < 2) (hDA : InDomainOfAttractionIndex μ α) : IsRegularlyVarying (combinedTail μ) (-α) ∧ ∃ (p : ℝ), HasTailBalance μ p

Converse direction: if μ is in the domain of attraction of a stable law of index α ∈ (0, 2), then the combined tail P(|X| > x) is regularly varying of index -α and the right/combined tail ratio has a limit (tail balance).

theorem ProbabilityTheory.domain_of_attraction_iff_tail_alpha_lt_two (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (α : ℝ) (hα₁ : 0 < α) (hα₂ : α < 2) : InDomainOfAttractionIndex μ α ↔ IsRegularlyVarying (combinedTail μ) (-α) ∧ ∃ (p : ℝ), HasTailBalance μ p

Domain of attraction characterization for α < 2. For 0 < α < 2, μ is in the domain of attraction of a stable law of index α if and only if combinedTail μ is regularly varying with index -α and the right/combined tail ratio has a limit.

theorem ProbabilityTheory.domain_of_attraction_iff_tail_alpha_eq_two (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (G : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure G] (hG : IsStable G 2) : InDomainOfAttraction μ G ↔ IsSlowlyVarying fun (x : ℝ) => ∫ (y : ℝ) in Set.Icc (-x) x, y ^ 2 ∂μ

Domain of attraction characterization for α = 2 (Gaussian case). For a stable law G of index 2 (Gaussian), μ lies in the domain of attraction of G if and only if the truncated second-moment function x ↦ ∫_{[-x, x]} y^2 dμ(y) is slowly varying.

theorem domain_of_attraction_theorem (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (α : ℝ) (hα₁ : 0 < α) (hα₂ : α < 2) : ProbabilityTheory.InDomainOfAttractionIndex μ α ↔ ProbabilityTheory.IsRegularlyVarying (ProbabilityTheory.combinedTail μ) (-α) ∧ ∃ (p : ℝ), ProbabilityTheory.HasTailBalance μ p

Theorem (Domain of attraction to stable random variable). Top-level wrapper: for 0 < α < 2, μ is in the domain of attraction of a stable law of index α iff its combined tail is regularly varying of index -α and tail balance holds.