InitialDensity.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

InitialDensity

Defect monomials, orthogonality, normalized initial densities, and common mass.

theorem OAI.TraceReconstruction.exists_unique_defect_tuple line 23
Source documentation
A monotone tuple of defect slots is uniquely identified by the retained ranks whenever all these ranks carry defects.
```
theorem exists_unique_defect_tuple {n l u r : ℕ}
    (d : Fin u → Fin n) (hd : StrictMono d) (v : IncreasingTuple l r)
    (S : FixedSubset (Fin n) l)
    (h : ∀ i, slotAtRank S (v.val i) ∈ Set.range d) :
    ∃! j : IncreasingTuple u r, taggedRankEvent (d ∘ j.val) v.val S := by
…
```
Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.FixedSubset, OAI.TraceReconstruction.slotAtRank, OAI.TraceReconstruction.taggedRankEvent
theorem OAI.TraceReconstruction.defect_tuple_indicator line 46
Source documentation
The degree coefficient is the sum over actual tagged defect tuples, not a separately postulated kernel array.
```
theorem defect_tuple_indicator {n l u r : ℕ}
    (d : Fin u → Fin n) (hd : StrictMono d) (v : IncreasingTuple l r)
    (S : FixedSubset (Fin n) l) :
    (if ∀ i, slotAtRank S (v.val i) ∈ Set.range d then (1:ℝ) else 0) =
      ∑ j : IncreasingTuple u r, if taggedRankEvent (d ∘ j.val) v.val S then 1 else 0 := by
…
```
Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.FixedSubset, OAI.TraceReconstruction.slotAtRank, OAI.TraceReconstruction.taggedRankEvent
def OAI.TraceReconstruction.rankDefectCoefficient line 74
theorem OAI.TraceReconstruction.rankDefectCoefficient_eq line 80
theorem OAI.TraceReconstruction.selected_defect_coefficient line 96
Source documentation
Bool-mask form of the selected-rank coefficient, in the exact multilinear density expansion.
```
theorem selected_defect_coefficient {n l : ℕ} (D : Finset (Fin n))
    (S : FixedSubset (Fin n) l) (σ : Fin l → Bool) :
    selectionCoefficient (defectAtRank D S) σ =
      if ∀ i, σ i = true → slotAtRank S i ∈ D then (1:ℝ) else 0 := by
…
```
Mentions: OAI.TraceReconstruction.FixedSubset, OAI.TraceReconstruction.selectionCoefficient, OAI.TraceReconstruction.defectAtRank, OAI.TraceReconstruction.slotAtRank
def OAI.TraceReconstruction.rankMask line 115
theorem OAI.TraceReconstruction.averaged_rank_coefficient line 118
def OAI.TraceReconstruction.tupleOfMask line 146
Source documentation
Canonical increasing tuple associated with a selected set of ranks.
```
def tupleOfMask {l r : ℕ} (σ : Fin l → Bool) (hσ : monomialDegree σ = r) :
    IncreasingTuple l r := by
…
```
Mentions: OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.IncreasingTuple
theorem OAI.TraceReconstruction.rankMask_tupleOfMask line 153
theorem OAI.TraceReconstruction.tupleOfMask_injective line 168
theorem OAI.TraceReconstruction.sum_degree_coeff_sq_le line 177
Source documentation
Changing from Boolean monomial labels to ordered rank tuples loses no mass; an injection suffices for the upper bounds.
```
theorem sum_degree_coeff_sq_le {l r : ℕ} (A : (Fin l → Bool) → ℝ) :
    (∑ σ : Fin l → Bool, if monomialDegree σ = r then A σ ^ 2 else 0) ≤
      ∑ v : IncreasingTuple l r, A (rankMask v)^2 := by
…
```
Mentions: OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.rankMask

theorem OAI.TraceReconstruction.multilinear_second_moment line 200

Source documentation

Exact orthogonality of the multilinear expansion; this avoids any loss in the channel power in consecutive-run overlap.

theorem multilinear_second_moment {α : Type*} [Fintype α] (P : FiniteLaw α)
    (Z : α → ℝ) (hcenter : P.expect Z = 0) (R : ℝ)
    (hvar : P.expect (fun a => Z a^2) = R^2) (n : ℕ)
    (A : (Fin n → Bool) → ℝ) :
    (P.product n).expect (fun x => multilinear A Z x ^ 2) =
      multilinearEnergy A R := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.multilinear, OAI.TraceReconstruction.multilinearEnergy

theorem OAI.TraceReconstruction.FiniteLaw.associated_totalPreorder line 243
Source documentation
Association requires only a total preorder, allowing tied likelihoods.
```
theorem FiniteLaw.associated_totalPreorder {α : Type*} [Fintype α] [Preorder α]
    (P : FiniteLaw α) (htotal : ∀ a b : α, a ≤ b ∨ b ≤ a) : P.Associated := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
theorem OAI.TraceReconstruction.averagedDensity_nonneg line 268
Source documentation
Conditional average densities are nonnegative when the coordinate likelihoods are nonnegative.
```
theorem averagedDensity_nonneg {α Ω : Type*} [Fintype Ω] {n : ℕ}
    (R : FiniteLaw Ω) (θ : Ω → Fin n → Bool) (Z : α → ℝ)
    (hZ : ∀ a, 0 ≤ 1+Z a) (x : Fin n → α) :
    0 ≤ averagedDensity R θ Z x := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.averagedDensity
theorem OAI.TraceReconstruction.averagedDensity_mono line 281
theorem OAI.TraceReconstruction.selectionDensity_mean line 299
Source documentation
Every independent-score likelihood product is normalized.
```
theorem selectionDensity_mean {α : Type*} [Fintype α] (P : FiniteLaw α)
    (Z : α → ℝ) (hZ : P.expect Z = 0) {n : ℕ} (θ : Fin n → Bool) :
    (P.product n).expect (selectionDensity θ Z) = 1 := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.selectionDensity
theorem OAI.TraceReconstruction.averagedDensity_mean line 312

theorem OAI.TraceReconstruction.multilinearEnergy_degrees line 334

Source documentation

Exact decomposition of the coefficient energy by its degree.

theorem multilinearEnergy_degrees {n : ℕ} (A : (Fin n → Bool) → ℝ) (R : ℝ) :
    multilinearEnergy A R = ∑ r ∈ Finset.range (n+1),
      R^(2*r) * ∑ σ : Fin n → Bool, if monomialDegree σ = r then A σ^2 else 0 := by
…

Mentions: OAI.TraceReconstruction.multilinearEnergy, OAI.TraceReconstruction.monomialDegree

theorem OAI.TraceReconstruction.monomialDegree_eq_zero_iff line 354
Source documentation
A zero-degree selection is precisely the empty selection.
```
theorem monomialDegree_eq_zero_iff {n : ℕ} (σ : Fin n → Bool) :
    monomialDegree σ = 0 ↔ σ = fun _ => false := by
…
```
Mentions: OAI.TraceReconstruction.monomialDegree
theorem OAI.TraceReconstruction.averaged_degree_zero line 370
theorem OAI.TraceReconstruction.increasingTuple_isEmpty line 378
Source documentation
There is no increasing selection with more entries than its ambient set.
```
theorem increasingTuple_isEmpty {n r : ℕ} (h : n < r) : IsEmpty (IncreasingTuple n r) := by
…
```
Mentions: OAI.TraceReconstruction.IncreasingTuple
theorem OAI.TraceReconstruction.defect_degree_bound line 386
Source documentation
The finite law of uniformly retained slots has no coefficients beyond its number of actual defect slots.
```
theorem defect_degree_bound {n l u r : ℕ} (hl : l ≤ n)
    (d : Fin u → Fin n) (hd : StrictMono d) (hru : u < r) :
    (∑ σ : Fin l → Bool, if monomialDegree σ = r then
      averagedCoefficient (uniformSubsetLaw l (by simpa using hl))
        (defectAtRank (Finset.univ.image d)) σ ^ 2 else 0) = 0 := by
…
```
Mentions: OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.averagedCoefficient, OAI.TraceReconstruction.uniformSubsetLaw, OAI.TraceReconstruction.defectAtRank

theorem OAI.TraceReconstruction.period_degree_square_sum line 403

Source documentation

Coefficient version of the conditional-rank square-sum estimate.

theorem period_degree_square_sum {u m l r : ℕ} (hl : l ≤ u*m) (hr : 0 < r)
    (hru : r ≤ u) (hm : 32 ≤ m) (hum : u ≤ m) {δ θ : ℝ}
    (hδ : δ ∈ Set.Ioc 0 (1/2:ℝ))
    (hθ : θ ∈ Set.Icc (1-δ^2) (1-δ^2/4))
    (hmean : ((u*m:ℕ):ℝ)*θ=l) (hv : 1 ≤ ((u*m:ℕ):ℝ)*θ*(1-θ))
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2) :
    (∑ σ : Fin l → Bool, if monomialDegree σ = r then
      averagedCoefficient (uniformSubsetLaw l (by simpa using hl))
        (defectAtRank (Finset.univ.image (periodSlot off))) σ ^ 2 else 0) ≤
      ((3*rankSchurConstant/δ)*Real.sqrt ((u:ℝ)/((m:ℝ)*r)))^r := by
…

Mentions: OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.averagedCoefficient, OAI.TraceReconstruction.uniformSubsetLaw, OAI.TraceReconstruction.defectAtRank, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.rankSchurConstant

theorem OAI.TraceReconstruction.period_density_energy line 423

Source documentation

The full coefficient energy is controlled by the subgaussian degree series, uniformly in the number of retained coordinates.

theorem period_density_energy {u m l : ℕ} (hl : l ≤ u*m)
    (hm : 32 ≤ m) (hum : u ≤ m) {δ θ : ℝ}
    (hδ : δ ∈ Set.Ioc 0 (1/2:ℝ))
    (hθ : θ ∈ Set.Icc (1-δ^2) (1-δ^2/4))
    (hmean : ((u*m:ℕ):ℝ)*θ=l) (hv : 1 ≤ ((u*m:ℕ):ℝ)*θ*(1-θ))
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2) (R : ℝ) :
    multilinearEnergy
      (averagedCoefficient (uniformSubsetLaw l (by simpa using hl))
        (defectAtRank (Finset.univ.image (periodSlot off)))) R ≤
      ∑ r ∈ Finset.range (l+1),
…

Mentions: OAI.TraceReconstruction.multilinearEnergy, OAI.TraceReconstruction.averagedCoefficient, OAI.TraceReconstruction.uniformSubsetLaw, OAI.TraceReconstruction.defectAtRank, OAI.TraceReconstruction.periodSlot

theorem OAI.TraceReconstruction.degree_series_le_exp line 461
Source documentation
A convenient exponential majorant for the full nonnegative degree series.
```
theorem degree_series_le_exp (a : ℝ) (N : ℕ) :
    (∑ r ∈ Finset.range N, a^r / (Real.sqrt (r:ℝ))^r) ≤ 2*Real.exp (a^2) := by
…
```

theorem OAI.TraceReconstruction.period_density_second_moment line 472

Source documentation

Actual conditional initial-oracle density, with its exact second moment.

theorem period_density_second_moment {α : Type*} [Fintype α]
    (P : FiniteLaw α) (Z : α → ℝ) (hZ : P.expect Z = 0)
    {u m l : ℕ} (hl : l ≤ u*m)
    (hm : 32 ≤ m) (hum : u ≤ m) {δ θ : ℝ}
    (hδ : δ ∈ Set.Ioc 0 (1/2:ℝ))
    (hθ : θ ∈ Set.Icc (1-δ^2) (1-δ^2/4))
    (hmean : ((u*m:ℕ):ℝ)*θ=l) (hv : 1 ≤ ((u*m:ℕ):ℝ)*θ*(1-θ))
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2) :
    (P.product l).expect (fun x =>
      averagedDensity (uniformSubsetLaw l (by simpa using hl))
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.averagedDensity, OAI.TraceReconstruction.uniformSubsetLaw

theorem OAI.TraceReconstruction.averagedDensity_overlap line 502

Source documentation

The source association argument holds for any two conditional mixture experiments using the same independent primitive marks, even when their retained-subset sample spaces have different original sizes.

theorem averagedDensity_overlap {α Ω Ψ : Type*}
    [Fintype α] [Fintype Ω] [Fintype Ψ]
    (P : FiniteLaw α) (R : FiniteLaw Ω) (S : FiniteLaw Ψ)
    (Z : α → ℝ) (hZ : P.expect Z = 0) (hZpos : ∀ a, 0 ≤ 1+Z a)
    {l : ℕ} (f : Ω → Fin l → Bool) (g : Ψ → Fin l → Bool) :
    (1:ℝ)/32 ≤
      (P.product l).expect (fun x => min (averagedDensity R f Z x) (averagedDensity S g Z x)) *
      (P.product l).expect (fun x => averagedDensity R f Z x ^ 2) *
      (P.product l).expect (fun x => averagedDensity S g Z x ^ 2) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.averagedDensity