Ranks.lean`

120 declarations, 0 contain sorry, 0 declared as axioms

Ranks

Retained subsets, conditional rank experiments, tagged gaps, period geometry, Gaussian Schur estimates, and uniform square sums.

def OAI.TraceReconstruction.subsetWeight line 24
theorem OAI.TraceReconstruction.sum_subsetWeight line 27
theorem OAI.TraceReconstruction.sum_fixedCard_subsetWeight line 32
def OAI.TraceReconstruction.subsetLaw line 50
abbrev OAI.TraceReconstruction.FixedSubset line 55
theorem OAI.TraceReconstruction.card_fixedSubset line 57
def OAI.TraceReconstruction.uniformSubsetLaw line 65
theorem OAI.TraceReconstruction.conditional_subset_uniform line 74
Source documentation
Conditional Bernoulli sampling, at every interior parameter, is exactly uniform.
```
theorem conditional_subset_uniform {p : ℝ} (hp : p ∈ Set.Ioo 0 1)
    {l : ℕ} (hl : l ≤ Fintype.card α) (S : FixedSubset α l) :
    subsetWeight p S.val / binomialMass (Fintype.card α) p l =
      (uniformSubsetLaw l hl).mass S := by
…
```
Mentions: OAI.TraceReconstruction.FixedSubset, OAI.TraceReconstruction.subsetWeight, OAI.TraceReconstruction.binomialMass, OAI.TraceReconstruction.uniformSubsetLaw
def OAI.TraceReconstruction.slotAtRank line 86
Source documentation
Slot at an observed return rank, with the original total order.
```
def slotAtRank {n l : ℕ} (S : FixedSubset (Fin n) l) (v : Fin l) : Fin n :=
…
```
Mentions: OAI.TraceReconstruction.FixedSubset
theorem OAI.TraceReconstruction.slotAtRank_mem line 89
theorem OAI.TraceReconstruction.slotAtRank_strictMono line 92
def OAI.TraceReconstruction.defectAtRank line 98
def OAI.TraceReconstruction.taggedRankEvent line 101
def OAI.TraceReconstruction.subsetRankKernel line 105
Source documentation
Unhypothesized rank kernel: defined from the actual uniformly retained subset.
```
def subsetRankKernel {n l r : ℕ} (hl : l≤n) (p : Fin r → Fin n) (v : Fin r → Fin l) : ℝ := by
…
```
theorem OAI.TraceReconstruction.subsetRankKernel_nonneg line 110
theorem OAI.TraceReconstruction.subsetRankKernel_le_one line 120
abbrev OAI.TraceReconstruction.GapUniverse line 134
Source documentation
Canonical slot universe split at the tagged positions. Actual order is only needed to identify each component with its before/between/after interval.
```
abbrev GapUniverse (r d : ℕ) (g : Fin d → ℕ) := Fin r ⊕ ((i : Fin d) × Fin (g i))
```
def OAI.TraceReconstruction.gapDecode line 136
def OAI.TraceReconstruction.gapEncode line 140
theorem OAI.TraceReconstruction.mem_gapEncode_left line 147
theorem OAI.TraceReconstruction.mem_gapEncode_right line 151
theorem OAI.TraceReconstruction.gapDecode_encode line 155
theorem OAI.TraceReconstruction.gapEncode_decode line 159
def OAI.TraceReconstruction.gapEvent line 167
instance OAI.TraceReconstruction.gapEvent_decidable line 171
def OAI.TraceReconstruction.gapEventEquiv line 176
theorem OAI.TraceReconstruction.card_gapEvent line 193
theorem OAI.TraceReconstruction.card_gapEncode line 200
theorem OAI.TraceReconstruction.card_of_gapEvent line 217
theorem OAI.TraceReconstruction.gapEvent_bernoulli_probability line 225
Source documentation
The exact unconditioned tagged-gap probability; no asymptotic estimate is used.
```
theorem gapEvent_bernoulli_probability {r d : ℕ} (g z : Fin d → ℕ)
    (hz : ∀ i, z i≤g i) (p : ℝ) :
    (∑ S : Finset (GapUniverse r d g), if gapEvent z S then subsetWeight p S else 0) =
      p^r * ∏ i, binomialMass (g i) p (z i) := by
…
```
Mentions: OAI.TraceReconstruction.GapUniverse, OAI.TraceReconstruction.gapEvent, OAI.TraceReconstruction.subsetWeight, OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.gapEvent_conditional_formula line 250

Source documentation

Conditional Bernoulli representation of the source rank kernel in gap coordinates.

theorem gapEvent_conditional_formula {r d : ℕ} (g z : Fin d → ℕ)
    (hz : ∀ i, z i≤g i) (p : ℝ) :
    (∑ S : Finset (GapUniverse r d g), if gapEvent z S then subsetWeight p S else 0) /
      binomialMass (r+∑ i, g i) p (r+∑ i, z i) =
    p^r / binomialMass (r+∑ i, g i) p (r+∑ i, z i) *
      ∏ i, binomialMass (g i) p (z i) := by
…

Mentions: OAI.TraceReconstruction.GapUniverse, OAI.TraceReconstruction.gapEvent, OAI.TraceReconstruction.subsetWeight, OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.slotAtRank_lower_card line 264
theorem OAI.TraceReconstruction.slotAtRank_eq_iff line 282
def OAI.TraceReconstruction.tupleLower line 298
Source documentation
Bounds for the open gaps of an increasing tuple; slots and ranks are zero-based.
```
def tupleLower {n r : ℕ} (p : Fin r → Fin n) : Fin (r+1) → ℕ :=
…
```
def OAI.TraceReconstruction.tupleUpper line 301
def OAI.TraceReconstruction.tupleGap line 304
theorem OAI.TraceReconstruction.tupleLower_zero line 307
theorem OAI.TraceReconstruction.tupleLower_succ line 309
theorem OAI.TraceReconstruction.tupleUpper_castSucc line 311
theorem OAI.TraceReconstruction.tupleUpper_last line 313
theorem OAI.TraceReconstruction.tupleLower_le_tag line 316
theorem OAI.TraceReconstruction.tag_lt_tupleLower line 329
theorem OAI.TraceReconstruction.tupleUpper_le_total line 342
theorem OAI.TraceReconstruction.tupleLower_le_total line 348
theorem OAI.TraceReconstruction.tupleLower_le_upper line 354
theorem OAI.TraceReconstruction.tupleGap_total line 360
def OAI.TraceReconstruction.tupleGapMap line 374
Source documentation
Maps abstract gap coordinates to their actual source slots.
```
def tupleGapMap {n r : ℕ} (p : Fin r → Fin n) :
    GapUniverse r (r+1) (tupleGap p) → Fin n
  | .inl i => p i
  | .inr ⟨j,a⟩ => ⟨tupleLower p j + a.val, by
      have hx := a.isLt
…
```
Mentions: OAI.TraceReconstruction.GapUniverse, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.tupleLower
theorem OAI.TraceReconstruction.tupleGapMap_gap_lt_tag line 383
theorem OAI.TraceReconstruction.tupleGapMap_tag_lt_gap line 404
theorem OAI.TraceReconstruction.tupleGapMap_injective line 417
def OAI.TraceReconstruction.tupleGapEquiv line 455

theorem OAI.TraceReconstruction.gapEncoded_lower_card line 463

Source documentation

The count below a tagged slot is its tag index plus the retained gap counts.

theorem gapEncoded_lower_card {n r : ℕ} (p : Fin r → Fin n) (hp : StrictMono p)
    (A : (j : Fin (r+1)) → Finset (Fin (tupleGap p j))) (i : Fin r) :
    (((gapEncode A).map (tupleGapEquiv p hp).toEmbedding).filter
      fun x => x < p i).card = i.val + ∑ j ∈ Finset.Iic i.castSucc, (A j).card := by
…

Mentions: OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.gapEncode, OAI.TraceReconstruction.tupleGapEquiv

theorem OAI.TraceReconstruction.gapEncode_univ line 499
theorem OAI.TraceReconstruction.tupleGap_prefix line 506

theorem OAI.TraceReconstruction.fin_prefix_sum_injective line 515

Source documentation

Initial-segment sums determine a family of natural numbers.

theorem fin_prefix_sum_injective {d : ℕ} (f g : Fin d → ℕ)
    (h : ∀ i, (∑ j ∈ Finset.Iic i, f j) = ∑ j ∈ Finset.Iic i, g j) : f=g := by
…

def OAI.TraceReconstruction.pullGapSet line 529
theorem OAI.TraceReconstruction.mem_pullGapSet line 533
theorem OAI.TraceReconstruction.map_pullGapSet line 538
theorem OAI.TraceReconstruction.pullGapSet_map line 544
theorem OAI.TraceReconstruction.pullGapSet_lower_card line 550
theorem OAI.TraceReconstruction.pullGapSet_total_card line 560
theorem OAI.TraceReconstruction.taggedRankEvent_iff_gapEvent line 570
instance OAI.TraceReconstruction.taggedRankEvent_decidable line 611
def OAI.TraceReconstruction.rankGapEventEquiv line 618
Source documentation
The actual event of seeing specified source slots at specified output ranks is in bijection with independent choices of the retained slots in each gap.
```
def rankGapEventEquiv {n l r : ℕ} (p : Fin r → Fin n) (hp : StrictMono p)
    (v : Fin r → Fin l) (hv : StrictMono v) :
    {S : FixedSubset (Fin n) l // taggedRankEvent p v S} ≃
      {T : Finset (GapUniverse r (r+1) (tupleGap p)) // gapEvent (tupleGap v) T} where
…
```
Mentions: OAI.TraceReconstruction.FixedSubset, OAI.TraceReconstruction.taggedRankEvent, OAI.TraceReconstruction.GapUniverse, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.gapEvent
theorem OAI.TraceReconstruction.card_taggedRankEvent line 638

theorem OAI.TraceReconstruction.subsetRankKernel_choose_formula line 646

Source documentation

Exact counting formula, including impossible rank/gap profiles.

theorem subsetRankKernel_choose_formula {n l r : ℕ} (hl : l ≤ n)
    (p : Fin r → Fin n) (hp : StrictMono p) (v : Fin r → Fin l) (hv : StrictMono v) :
    subsetRankKernel hl p v =
      (∏ j, ((tupleGap p j).choose (tupleGap v j) : ℝ)) / (n.choose l : ℝ) := by
…

Mentions: OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.tupleGap

theorem OAI.TraceReconstruction.gapEvent_conditional_choose line 657
theorem OAI.TraceReconstruction.subsetRankKernel_binomial_formula line 684
Source documentation
Conditional product formula for the kernel defined from actual retained subsets, not an assumed auxiliary kernel. Source the initial-pair construction 50–62.
```
theorem subsetRankKernel_binomial_formula {n l r : ℕ} (hl : l ≤ n)
    (p : Fin r → Fin n) (hp : StrictMono p) (v : Fin r → Fin l) (hv : StrictMono v)
    (θ : ℝ) (hθ : θ ∈ Set.Ioo 0 1) :
    subsetRankKernel hl p v = θ^r / binomialMass n θ l *
      ∏ j, binomialMass (tupleGap p j) θ (tupleGap v j) := by
…
```
Mentions: OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.binomialMass, OAI.TraceReconstruction.tupleGap
def OAI.TraceReconstruction.coarsePeriodGap line 710
Source documentation
Twice the coarse period gaps (endpoints are half-integral before doubling).
```
def coarsePeriodGap {u r : ℕ} (j : Fin r → Fin u) (i : Fin (r+1)) : ℕ :=
…
```
theorem OAI.TraceReconstruction.coarsePeriodGap_pos line 713
theorem OAI.TraceReconstruction.coarsePeriodGap_sum line 718
theorem OAI.TraceReconstruction.coarsePeriodGap_le line 739
theorem OAI.TraceReconstruction.tupleGap_injective line 744
theorem OAI.TraceReconstruction.coarsePeriodGap_injective line 753
def OAI.TraceReconstruction.periodSlot line 763
Source documentation
Actual defect slot in a period, with zero-based period and slot indices.
```
def periodSlot {u m : ℕ} (off : Fin u → Fin m) (j : Fin u) : Fin (u*m) :=
…
```
theorem OAI.TraceReconstruction.periodSlot_strictMono line 769
theorem OAI.TraceReconstruction.tupleGap_zero line 778
theorem OAI.TraceReconstruction.tupleGap_last line 784
theorem OAI.TraceReconstruction.tupleGap_middle line 789
theorem OAI.TraceReconstruction.coarsePeriodGap_zero line 794
theorem OAI.TraceReconstruction.coarsePeriodGap_last line 798
theorem OAI.TraceReconstruction.coarsePeriodGap_middle line 802

theorem OAI.TraceReconstruction.period_gap_rounding line 812

Source documentation

Actual bounded defect displacements give the O(1) gap errors of the initial-pair construction.

theorem period_gap_rounding {u m r : ℕ} (hr : 0 < r)
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2)
    (j : Fin r → Fin u) (hj : StrictMono j) (i : Fin (r+1)) :
    |(tupleGap (periodSlot off ∘ j) i:ℝ) - (m:ℝ)*coarsePeriodGap j i/2| ≤ 4 := by
…

Mentions: OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.coarsePeriodGap

abbrev OAI.TraceReconstruction.IncreasingTuple line 858
Source documentation
An increasing tuple enumerates a monomial's distinct observed ranks.
```
abbrev IncreasingTuple (n r : ℕ) := {v : Fin r → Fin n // StrictMono v}
```
instance OAI.TraceReconstruction.increasingTupleFintype line 860
theorem OAI.TraceReconstruction.tupleGap_le_remainder line 863
def OAI.TraceReconstruction.rankGapProfile line 870
theorem OAI.TraceReconstruction.rankGapProfile_sum line 874
theorem OAI.TraceReconstruction.rankGapProfile_injective line 881

theorem OAI.TraceReconstruction.sum_injective_profile_le line 897

Source documentation

Summing nonnegative kernels over actual profiles may drop any remaining constraints.

theorem sum_injective_profile_le {α β : Type*} [Fintype α] [Fintype β]
    (profile : α → β) (hinj : Function.Injective profile)
    (P : β → Prop) [DecidablePred P] (hp : ∀ a, P (profile a))
    (f : β → ℝ) (hf : ∀ b, 0 ≤ f b) :
    (∑ a, f (profile a)) ≤ ∑ b, if P b then f b else 0 := by
…

theorem OAI.TraceReconstruction.subsetRankKernel_cross_le line 924

Source documentation

The actual conditional rank kernel, summed over distinct observed ranks, reduces to the constrained finite product estimate with any eliminated gap.

theorem subsetRankKernel_cross_le {n l r : ℕ} (hl : l ≤ n)
    (p q : Fin r → Fin n) (hp : StrictMono p) (hq : StrictMono q)
    (θ : ℝ) (hθ : θ ∈ Set.Ioo 0 1) (e : Fin (r+1))
    (M : ℝ) (hM : 0 ≤ M)
    (hbound : ∀ k : Fin (l-r+1),
      binomialMass (tupleGap p e) θ k * binomialMass (tupleGap q e) θ k ≤ M) :
    (∑ v : IncreasingTuple l r,
      subsetRankKernel hl p v.val * subsetRankKernel hl q v.val) ≤
      (θ^r / binomialMass n θ l)^2 * M *
        ∏ i : Fin r, ∑ k : Fin (l-r+1),
          binomialMass (tupleGap p (Equiv.swap 0 e i.succ)) θ k *
          binomialMass (tupleGap q (Equiv.swap 0 e i.succ)) θ k := by
…

Mentions: OAI.TraceReconstruction.binomialMass, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.subsetRankKernel

theorem OAI.TraceReconstruction.finite_geometric_distance line 980
theorem OAI.TraceReconstruction.finite_gaussian_distance line 1000
theorem OAI.TraceReconstruction.fin_geometric_distance line 1026
theorem OAI.TraceReconstruction.coarse_laplace_sum_with_zero line 1034

theorem OAI.TraceReconstruction.coarse_constrained_inverse_sum line 1046

Source documentation

The total constraint eliminates one coarse gap with no cost in its size. The zero-extension of x^(-1/2) avoids any singular integral convention.

theorem coarse_constrained_inverse_sum (r U : ℕ) {h : ℝ} (hh : 0<h) (h1 : h≤1) :
    (∑ γ : Fin (r+1) → Fin (U+1),
      if ∑ i, (γ i).val=U then ∏ i : Fin r, (Real.sqrt ((γ i.succ).val:ℝ))⁻¹ else 0) ≤
      Real.exp (h*U) * (6/Real.sqrt h)^r := by
…

theorem OAI.TraceReconstruction.sum_sq_sum_kernel line 1104

Source documentation

The squared norm of an aggregate equals the sum of the cross-kernels.

theorem sum_sq_sum_kernel {α β : Type*} [Fintype β] (S : Finset α) (K : α → β → ℝ) :
    (∑ z, (∑ a ∈ S, K a z)^2) =
      ∑ a ∈ S, ∑ b ∈ S, ∑ z, K a z*K b z := by
…

theorem OAI.TraceReconstruction.coarse_kernel_square_sum line 1115

Source documentation

Schur summation over all pairs of coarse-gap profiles, retaining the largest-gap total constraint before dropping other restrictions.

theorem coarse_kernel_square_sum {β : Type*} [Fintype β] (r U : ℕ)
    (S : Finset (Fin (r+1) → Fin (U+1)))
    (K : (Fin (r+1) → Fin (U+1)) → β → ℝ) {M ρ h : ℝ}
    (hM : 0≤M) (hρ : ρ∈Set.Ico 0 1) (hh : 0<h) (h1 : h≤1)
    (hS : ∀ γ∈S, ∑ i, (γ i).val=U)
    (hcross : ∀ γ∈S, ∀ γ'∈S, (∑ z, K γ z*K γ' z) ≤
      M * ∏ i:Fin r, ((Real.sqrt ((γ i.succ).val:ℝ))⁻¹ *
        ρ^(((γ' i.succ).val:ℤ)-(γ i.succ).val).natAbs)) :
    (∑ z, (∑ γ∈S, K γ z)^2) ≤
      M * (2/(1-ρ))^r * Real.exp (h*U) * (6/Real.sqrt h)^r := by
…

theorem OAI.TraceReconstruction.coarse_kernel_rectangular_sum line 1192

theorem OAI.TraceReconstruction.coarse_gap_geometry line 1276

Source documentation

Geometry of actual period gaps: the half-integer coarse gaps are represented by positive integers a,b, with bounded slot-rounding errors.

theorem coarse_gap_geometry (m U a b g k : ℕ) (hm : 32 ≤ m) (hUm : U  ≤  2*m)
    (ha : 1 ≤ a) (hb : 1 ≤ b) (haU : a ≤ U) (hbU : b ≤ U)
    (hg : |(g:ℝ)-(m:ℝ)*a/2| ≤ 4) (hk : |(k:ℝ)-(m:ℝ)*b/2| ≤ 4) :
    (m:ℝ)*a/4  ≤  (g:ℝ)+1 ∧ 0<(g:ℝ)+k ∧
      ((a:ℝ)-b)^2/1024  ≤  ((g:ℝ)-k)^2/(16*((g:ℝ)+k)) := by
…

theorem OAI.TraceReconstruction.exp_integer_square_le line 1331

Source documentation

From integer Gaussian decay to a summable geometric profile.

theorem exp_integer_square_le (a b : ℕ) {c : ℝ} (hc : 0 ≤ c) :
    Real.exp (-c * ((a:ℝ)-b)^2) ≤
      (Real.exp (-c)) ^ ((a:ℤ)-b).natAbs := by
…

theorem OAI.TraceReconstruction.coarse_binomial_overlap line 1347
theorem OAI.TraceReconstruction.int_natAbs_sub_comm line 1389
theorem OAI.TraceReconstruction.subsetRankKernel_cross_normalized line 1392
def OAI.TraceReconstruction.periodProfile line 1430
theorem OAI.TraceReconstruction.periodProfile_sum line 1435
theorem OAI.TraceReconstruction.periodProfile_injective line 1441
theorem OAI.TraceReconstruction.period_kernel_cross line 1450
theorem OAI.TraceReconstruction.coarse_profile_geometric_sum line 1523
theorem OAI.TraceReconstruction.coarse_profile_inverse_sum line 1552

theorem OAI.TraceReconstruction.coarse_profile_bilinear_sum line 1565

Source documentation

Coarse Schur bound for actual injective profiles, with no extension of kernels outside their geometric domain.

theorem coarse_profile_bilinear_sum {α β : Type*} [Fintype α] [Fintype β]
    (r U : ℕ) (p : α → Fin (r+1) → Fin (U+1)) (q : β → Fin (r+1) → Fin (U+1))
    (hp : Function.Injective p) (hq : Function.Injective q)
    (hpt : ∀ a, ∑ i, (p a i).val=U) (hqt : ∀ b, ∑ i, (q b i).val=U)
    (K : α → β → ℝ) {M ρ h : ℝ}
    (hM : 0≤M) (hρ : ρ∈Set.Ico 0 1) (hh : 0<h) (h1 : h≤1)
    (hcross : ∀ a b, K a b ≤ M * ∏ i : Fin r,
      (Real.sqrt ((p a i.succ).val:ℝ))⁻¹ *
        ρ^(((q b i.succ).val:ℤ)-(p a i.succ).val).natAbs) :
    (∑ a, ∑ b, K a b) ≤ M*(2/(1-ρ))^r * Real.exp (h*U)*(6/Real.sqrt h)^r := by
…

def OAI.TraceReconstruction.LargePeriodTuple line 1603
instance OAI.TraceReconstruction.largePeriodTupleFintype line 1606
theorem OAI.TraceReconstruction.exists_large_period_gap line 1611

theorem OAI.TraceReconstruction.period_rank_square_sum_raw line 1623

Source documentation

Unnormalized but explicit source rank-kernel square-sum estimate. The only remaining factors are elementary scale simplifications.

theorem period_rank_square_sum_raw {u m l r : ℕ} (hl : l ≤ u*m) (hr : 0 < r)
    (hm : 32 ≤ m) (hum : u ≤ m) {θ h : ℝ} (hθ : θ ∈ Set.Ico (1/2:ℝ) 1)
    (hmean : ((u*m:ℕ):ℝ)*θ=l) (hv : 1 ≤ ((u*m:ℕ):ℝ)*θ*(1-θ))
    (hh : 0 < h) (h1 : h ≤ 1)
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2) :
    (∑ v : IncreasingTuple l r,
      (∑ j : IncreasingTuple u r, subsetRankKernel hl (periodSlot off ∘ j.val) v.val)^2) ≤
      9216*(r+1:ℕ)^2 * (Real.sqrt (8/((m:ℝ)*θ*(1-θ))))^r *
        (2/(1-Real.exp (-(1/1024:ℝ))))^r * Real.exp (h*(2*u:ℕ)) * (6/Real.sqrt h)^r := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.periodSlot

theorem OAI.TraceReconstruction.rank_polynomial_factor line 1695
def OAI.TraceReconstruction.rankSchurConstant line 1707
theorem OAI.TraceReconstruction.rankSchurConstant_pos line 1710

theorem OAI.TraceReconstruction.period_rank_square_sum line 1717

Source documentation

Rank-kernel square sum, with an explicit absolute constant, uniformly in the defect types and admissible conditional count.

theorem period_rank_square_sum {u m l r : ℕ} (hl : l ≤ u*m) (hr : 0 < r)
    (hru : r ≤ u) (hm : 32 ≤ m) (hum : u ≤ m) {θ : ℝ} (hθ : θ ∈ Set.Ico (1/2:ℝ) 1)
    (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) :
    (∑ v : IncreasingTuple l r,
      (∑ j : IncreasingTuple u r, subsetRankKernel hl (periodSlot off ∘ j.val) v.val)^2) ≤
      (rankSchurConstant * Real.sqrt ((u:ℝ)/((m:ℝ)*r*θ*(1-θ))))^r := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.rankSchurConstant

theorem OAI.TraceReconstruction.period_rank_square_sum_delta line 1781

Source documentation

The source's channel-uniform rank-kernel estimate (base-kernel), with the absolute constant made explicit.

theorem period_rank_square_sum_delta {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) :
    (∑ v : IncreasingTuple l r,
      (∑ j : IncreasingTuple u r, subsetRankKernel hl (periodSlot off ∘ j.val) v.val)^2) ≤
      ((3*rankSchurConstant/δ) * Real.sqrt ((u:ℝ)/((m:ℝ)*r)))^r := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.rankSchurConstant