FiniteStatistics.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite character tests determine joint statistics

This is the finite Fourier inversion step in sections/distribution.tex. It is an algebraic transfer lemma, not an assumed arithmetic decorrelation result. The arithmetic correlation limits still have to be established.

def OAI.JointDickman.weightedMean line 21

Source documentation

A finite weighted mean, as a linear statistic.

noncomputable def weightedMean {G : Type*} [Fintype G] (μ : G → ℂ) :
    (G → ℂ) →ₗ[ℂ] ℂ where
…

def OAI.JointDickman.productMean line 28

Source documentation

The product of the two marginal statistics.

noncomputable def productMean {G H : Type*}
    (μ : (G → ℂ) →ₗ[ℂ] ℂ) (ν : (H → ℂ) →ₗ[ℂ] ℂ) :
    (G → ℂ) →ₗ[ℂ] (H → ℂ) →ₗ[ℂ] ℂ where
…

def OAI.JointDickman.jointStatistic line 40
Source documentation
The ordinary empirical joint statistic; s is the counting range and w is the normalization. The observations may depend on the scale.
```
noncomputable def jointStatistic {G H : Type*} (s : Finset ℕ) (w : ℂ)
    (u : ℕ → G) (v : ℕ → H) :
    (G → ℂ) →ₗ[ℂ] (H → ℂ) →ₗ[ℂ] ℂ where
…
```
theorem OAI.JointDickman.linear_expansion line 50

theorem OAI.JointDickman.tendsto_linear_of_basis line 59

Source documentation

Convergence of linear statistics on a finite basis determines every statistic.

theorem tendsto_linear_of_basis {ι E : Type*} [Fintype ι]
    [AddCommGroup E] [Module ℂ E] (b : Basis ι ℂ E)
    (Q : ℕ → E →ₗ[ℂ] ℂ) (L : E →ₗ[ℂ] ℂ)
    (h : ∀ i, Tendsto (fun N => Q N (b i)) atTop (𝓝 (L (b i))))
    (v : E) : Tendsto (fun N => Q N v) atTop (𝓝 (L v)) := by
…

theorem OAI.JointDickman.tendsto_bilinear_of_bases line 68

Source documentation

Convergence on all pairs of finite basis vectors determines a bilinear statistic.

theorem tendsto_bilinear_of_bases {ι κ E F : Type*} [Fintype ι] [Fintype κ]
    [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F]
    (b : Basis ι ℂ E) (c : Basis κ ℂ F)
    (Q : ℕ → E →ₗ[ℂ] F →ₗ[ℂ] ℂ) (L : E →ₗ[ℂ] F →ₗ[ℂ] ℂ)
    (h : ∀ i j, Tendsto (fun N => Q N (b i) (c j)) atTop (𝓝 (L (b i) (c j))))
    (v : E) (w : F) : Tendsto (fun N => Q N v w) atTop (𝓝 (L v w)) := by
…

theorem OAI.JointDickman.tendsto_of_character_pairs line 80

Source documentation

For the finite bin-count group, character-pair limits imply limits for every pair of bin events. This does not assert those character-pair limits.

theorem tendsto_of_character_pairs {G H : Type*}
    [AddCommGroup G] [Fintype G] [AddCommGroup H] [Fintype H]
    (Q : ℕ → (G → ℂ) →ₗ[ℂ] (H → ℂ) →ₗ[ℂ] ℂ)
    (L : (G → ℂ) →ₗ[ℂ] (H → ℂ) →ₗ[ℂ] ℂ)
    (h : ∀ (χ : AddChar G ℂ) (ψ : AddChar H ℂ),
      Tendsto (fun N => Q N χ ψ) atTop (𝓝 (L χ ψ)))
    (f : G → ℂ) (g : H → ℂ) :
    Tendsto (fun N => Q N f g) atTop (𝓝 (L f g)) := by
…

theorem OAI.JointDickman.jointStatistic_factorization line 93

Source documentation

The concrete empirical form of finite Fourier inversion. Every pair of test functions has the product limit once every pair of characters does.

theorem jointStatistic_factorization {G H : Type*}
    [AddCommGroup G] [Fintype G] [AddCommGroup H] [Fintype H]
    (s : ℕ → Finset ℕ) (w : ℕ → ℂ) (u : ℕ → ℕ → G) (v : ℕ → ℕ → H)
    (μ : G → ℂ) (ν : H → ℂ)
    (h : ∀ (χ : AddChar G ℂ) (ψ : AddChar H ℂ),
      Tendsto (fun N => w N * ∑ n ∈ s N, χ (u N n) * ψ (v N n)) atTop
        (𝓝 ((∑ a, μ a * χ a) * (∑ b, ν b * ψ b))))
    (f : G → ℂ) (g : H → ℂ) :
    Tendsto (fun N => w N * ∑ n ∈ s N, f (u N n) * g (v N n)) atTop
      (𝓝 ((∑ a, μ a * f a) * (∑ b, ν b * g b))) := by
…

theorem OAI.JointDickman.jointEvent_factorization line 109

Source documentation

In particular, all pairs of events factor. These are precisely the bin events used to test smoothness at rational powers.

theorem jointEvent_factorization {G H : Type*}
    [AddCommGroup G] [Fintype G] [AddCommGroup H] [Fintype H]
    (s : ℕ → Finset ℕ) (w : ℕ → ℂ) (u : ℕ → ℕ → G) (v : ℕ → ℕ → H)
    (μ : G → ℂ) (ν : H → ℂ)
    (h : ∀ (χ : AddChar G ℂ) (ψ : AddChar H ℂ),
      Tendsto (fun N => w N * ∑ n ∈ s N, χ (u N n) * ψ (v N n)) atTop
        (𝓝 ((∑ a, μ a * χ a) * (∑ b, ν b * ψ b))))
    (A : G → Prop) (B : H → Prop) [DecidablePred A] [DecidablePred B] :
    Tendsto (fun N => w N * ∑ n ∈ s N,
      (if A (u N n) ∧ B (v N n) then (1 : ℂ) else 0)) atTop
      (𝓝 ((∑ a with A a, μ a) * (∑ b with B b, ν b))) := by
…