ArctanCenter.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Arctangent centers of probability laws

Every real probability law has a unique arctangent center without moment assumptions. The center depends only on the law, is translation-equivariant, and is continuous for weak convergence. Convergence of translated log-diameter laws yields scalar normalization limits; no FK/spanning-tree GHP convergence theorem is asserted.

def OAI.MetricMeasureLimits.DiameterCenter.score line 21
Source documentation
Expected arctangent after centering at a deterministic real number.
```
def score (μ : ProbabilityMeasure ℝ) (t : ℝ) : ℝ :=
…
```
lemma OAI.MetricMeasureLimits.DiameterCenter.norm_arctan_le line 24
lemma OAI.MetricMeasureLimits.DiameterCenter.integrable_score line 28
lemma OAI.MetricMeasureLimits.DiameterCenter.continuous_score line 34
lemma OAI.MetricMeasureLimits.DiameterCenter.strictAnti_score line 44
lemma OAI.MetricMeasureLimits.DiameterCenter.tendsto_score_atTop line 61
lemma OAI.MetricMeasureLimits.DiameterCenter.tendsto_score_atBot line 76
theorem OAI.MetricMeasureLimits.DiameterCenter.existsUnique_center line 93
Source documentation
Every real probability law has a unique arctangent center, without a moment assumption. This is the existence/uniqueness part of measure:center.
```
theorem existsUnique_center (μ : ProbabilityMeasure ℝ) :
    ∃! t : ℝ, score μ t = 0 := by
…
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.score
def OAI.MetricMeasureLimits.DiameterCenter.center line 106
Source documentation
The center is a function of the unconditional probability law alone.
```
def center (μ : ProbabilityMeasure ℝ) : ℝ := (existsUnique_center μ).choose
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.existsUnique_center
theorem OAI.MetricMeasureLimits.DiameterCenter.score_center line 108
lemma OAI.MetricMeasureLimits.DiameterCenter.center_eq_of_score_eq_zero line 111
lemma OAI.MetricMeasureLimits.DiameterCenter.score_pos_iff line 115
lemma OAI.MetricMeasureLimits.DiameterCenter.score_neg_iff line 119
def OAI.MetricMeasureLimits.DiameterCenter.translate line 124
Source documentation
Push a probability law forward by translation by c.
```
def translate (μ : ProbabilityMeasure ℝ) (c : ℝ) : ProbabilityMeasure ℝ :=
…
```
lemma OAI.MetricMeasureLimits.DiameterCenter.score_translate line 127
theorem OAI.MetricMeasureLimits.DiameterCenter.center_translate line 140
Source documentation
Translation equivariance in measure:center.
```
theorem center_translate (μ : ProbabilityMeasure ℝ) (c : ℝ) :
    center (translate μ c) = center μ + c := by
…
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.center, OAI.MetricMeasureLimits.DiameterCenter.translate
def OAI.MetricMeasureLimits.DiameterCenter.arctanTest line 146
Source documentation
A bounded continuous arctangent test of a law.
```
def arctanTest (t : ℝ) : ℝ →ᵇ ℝ :=
…
```
lemma OAI.MetricMeasureLimits.DiameterCenter.continuous_score_law line 157
theorem OAI.MetricMeasureLimits.DiameterCenter.tendsto_center line 162
Source documentation
Continuity under weak convergence of real probability laws in measure:center. The filter is arbitrary, not just a filter on subsequences.
```
theorem tendsto_center {ι : Type*} {l : Filter ι} {μs : ι → ProbabilityMeasure ℝ}
    {μ : ProbabilityMeasure ℝ} (h : Tendsto μs l (𝓝 μ)) :
    Tendsto (fun i => center (μs i)) l (𝓝 (center μ)) := by
…
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.center
theorem OAI.MetricMeasureLimits.DiameterCenter.continuous_center line 179
Source documentation
The no-moment arctangent center is continuous for the usual weak topology on probability measures.
```
theorem continuous_center : Continuous center := by
…
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.center
lemma OAI.MetricMeasureLimits.DiameterCenter.score_map line 190
Source documentation
Rewriting the law-level score as an expectation on a probability space. Only measurability, not integrability of the random variable, is needed.
```
lemma score_map (P : ProbabilityMeasure Ω) (Y : Ω → ℝ)
    (hY : AEMeasurable Y (P : Measure Ω)) (t : ℝ) :
    score (P.map Y) t = ∫ ω, Real.arctan (Y ω - t) ∂(P : Measure Ω) := by
…
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.score
theorem OAI.MetricMeasureLimits.DiameterCenter.existsUnique_randomVariable_center line 201
Source documentation
The existence/uniqueness assertion of measure:center for an arbitrary finite real random variable. The defining expectation is with respect to its unconditional probability law.
```
theorem existsUnique_randomVariable_center (P : ProbabilityMeasure Ω) (Y : Ω → ℝ)
    (hY : AEMeasurable Y (P : Measure Ω)) :
    ∃! m : ℝ, (∫ ω, Real.arctan (Y ω - m) ∂(P : Measure Ω)) = 0 := by
…
```

theorem OAI.MetricMeasureLimits.DiameterCenter.center_eq_of_law_eq line 208

Source documentation

Law equality implies equality of the centers; a change of probability space causes no ambiguity.

theorem center_eq_of_law_eq {Ω' : Type*} [MeasurableSpace Ω']
    (P : ProbabilityMeasure Ω) (Y : Ω → ℝ) (_hY : AEMeasurable Y (P : Measure Ω))
    (P' : ProbabilityMeasure Ω') (Y' : Ω' → ℝ) (_hY' : AEMeasurable Y' (P' : Measure Ω'))
    (h : P.map Y = P'.map Y') : center (P.map Y) = center (P'.map Y') :=
…

Mentions: OAI.MetricMeasureLimits.DiameterCenter.center

def OAI.MetricMeasureLimits.DiameterCenter.diameterScale line 224
Source documentation
The deterministic scale exp(m(ν) - m(τ)) from the normalization lemma.
```
def diameterScale (ν τ : ProbabilityMeasure ℝ) : ℝ :=
…
```
lemma OAI.MetricMeasureLimits.DiameterCenter.diameterScale_pos line 227
lemma OAI.MetricMeasureLimits.DiameterCenter.inv_diameterScale_pos line 231
Source documentation
The proposed distance rescaling is positive even when no moments exist.
```
lemma inv_diameterScale_pos (ν τ : ProbabilityMeasure ℝ) : 0 < (diameterScale ν τ)⁻¹ :=
…
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.diameterScale
theorem OAI.MetricMeasureLimits.DiameterCenter.tendsto_diameterScale_ratio line 238
Source documentation
Along any already-established convergence of the centered log-diameter laws, the deterministic scale ratio converges to the deterministic multiplier. This is the scalar step in measure:normalization, not the subsequential geometric/probabilistic input required by thm:main.
```
theorem tendsto_diameterScale_ratio {ι : Type*} {l : Filter ι}
    (ν : ι → ProbabilityMeasure ℝ) (τ : ProbabilityMeasure ℝ)
    (s : ι → ℝ) (hs : ∀ i, 0 < s i) (c : ℝ) (hc : 0 < c)
    (h : Tendsto (fun i => translate (ν i) (-Real.log (s i))) l
      (𝓝 (translate τ (Real.log c)))) :
    Tendsto (fun i => diameterScale (ν i) τ / s i) l (𝓝 c) := by
…
```
Mentions: OAI.MetricMeasureLimits.DiameterCenter.translate, OAI.MetricMeasureLimits.DiameterCenter.diameterScale

theorem OAI.MetricMeasureLimits.DiameterCenter.tendsto_inv_diameterScale_zero line 258

Source documentation

Reciprocal scales tend to zero along such a subsequence when its reference scale tends to infinity. This conclusion concerns only real numbers; no GHP convergence is assumed or asserted.

theorem tendsto_inv_diameterScale_zero {ι : Type*} {l : Filter ι}
    (ν : ι → ProbabilityMeasure ℝ) (τ : ProbabilityMeasure ℝ)
    (s : ι → ℝ) (hs : ∀ i, 0 < s i) (c : ℝ) (hc : 0 < c)
    (h : Tendsto (fun i => translate (ν i) (-Real.log (s i))) l
      (𝓝 (translate τ (Real.log c)))) (hsInf : Tendsto s l atTop) :
    Tendsto (fun i => (diameterScale (ν i) τ)⁻¹) l (𝓝 (0 : ℝ)) := by
…

Mentions: OAI.MetricMeasureLimits.DiameterCenter.translate, OAI.MetricMeasureLimits.DiameterCenter.diameterScale