InitialMoments.lean`

81 declarations, 0 contain sorry, 0 declared as axioms

InitialMoments

Initial coefficient tails, primitive conditioning, mark-list oracle densities, pure norm estimates, and moment energies.

theorem OAI.TraceReconstruction.signedPeriodDefects_comp line 22
def OAI.TraceReconstruction.signedTupleKernel line 31
theorem OAI.TraceReconstruction.signedRankCoefficient_tuple_sum line 38
theorem OAI.TraceReconstruction.signedTupleKernel_expansion line 47
def OAI.TraceReconstruction.clippedSignedRankCoefficient line 62
def OAI.TraceReconstruction.clippedPatternCoefficient line 67
theorem OAI.TraceReconstruction.clippedSignedRankCoefficient_expansion line 75
theorem OAI.TraceReconstruction.signedTupleKernel_tail line 105
Source documentation
Removing coarse rank rectangles loses an explicitly exponentially small amount in the actual coefficient, before any finite differences.
```
theorem signedTupleKernel_tail {u m l r : ℕ}
    (hu : 0 < u) (hm : 128 ≤ m) (hr : 0 < r) (hl : l ≤ u*m)
    (off : Fin m) (hoff : |(off.val:ℝ)-(m:ℝ)/2|≤3)
    (hsafe : SafeTaggedTuple (periodSlot (u := u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.motif_pattern_common_short_gap line 158
theorem OAI.TraceReconstruction.clipped_linear_pattern_norm line 179
theorem OAI.TraceReconstruction.clipped_nonlinear_pattern_norm line 203
def OAI.TraceReconstruction.signedPatternBound line 229
theorem OAI.TraceReconstruction.sum_square_card_bound line 236
theorem OAI.TraceReconstruction.clipped_signed_initial_norm line 248
theorem OAI.TraceReconstruction.signedRankCoefficient_tail line 287
theorem OAI.TraceReconstruction.finite_sum_sq_le_abs_sum_sq line 318
Source documentation
A globally discarded l1 tail is also negligible in coefficient energy. This does not assume pointwise cancellation on the discarded ranks.
```
theorem finite_sum_sq_le_abs_sum_sq {α : Type*} [Fintype α] (f : α → ℝ) :
    (∑a, f a^2) ≤ (∑a, |f a|)^2 := by
…
```
theorem OAI.TraceReconstruction.initial_signed_energy line 324

def OAI.TraceReconstruction.listDeletionExpectation line 363

Source documentation

Exact complete-trace expectation, recursively on the actual binary word.

def listDeletionExpectation (q : ℝ) : List Bool → (List Bool → ℝ) → ℝ
  | [], F => F []
  | b::w, F => q*listDeletionExpectation q w F +
      (1-q)*listDeletionExpectation q w (fun t => F (b::t))

theorem OAI.TraceReconstruction.traceOfMask_cons line 368
theorem OAI.TraceReconstruction.maskWeight_cons line 375
theorem OAI.TraceReconstruction.listDeletionExpectation_ofFn line 379
theorem OAI.TraceReconstruction.listDeletionExpectation_append line 394
def OAI.TraceReconstruction.primitiveBlock line 402
Source documentation
The primitive alphabet consists of the literal strings 01 and 1.
```
def primitiveBlock (b : Bool) : List Bool := if b then [true] else [false,true]
```
theorem OAI.TraceReconstruction.primitiveBlock_expectation line 404
theorem OAI.TraceReconstruction.primitiveBlock_erasure_expectation line 411
def OAI.TraceReconstruction.silentMarkExpectation line 425
Source documentation
Independent silent block erasures and conditionally emitted primitive marks. An emitted empty mark is retained in the list and differs from a silent erasure.
```
def silentMarkExpectation (q : ℝ) : List Bool → (List PrimitiveMark → ℝ) → ℝ
  | [], F => F []
  | b::bs, F => primitiveErasure q*silentMarkExpectation q bs F +
      (1-primitiveErasure q)*∑z : PrimitiveMark, primitiveMarkMass q b z*
        silentMarkExpectation q bs (fun ys => F (z::ys))
```
Mentions: OAI.TraceReconstruction.PrimitiveMark, OAI.TraceReconstruction.primitiveErasure, OAI.TraceReconstruction.primitiveMarkMass
def OAI.TraceReconstruction.joinPrimitiveMarks line 431
theorem OAI.TraceReconstruction.silentMarkExpectation_linear line 433
theorem OAI.TraceReconstruction.silentMarkExpectation_sum line 451
theorem OAI.TraceReconstruction.silentMarkExpectation_scale line 461
theorem OAI.TraceReconstruction.primitive_run_simulation line 469
Source documentation
The common deterministic mark-joining simulator is exact for arbitrary concatenations of primitive blocks; block boundaries are not reported.
```
theorem primitive_run_simulation {q : ℝ} (hq : q∈Set.Ioo 0 1)
    (bs : List Bool) (F : List Bool → ℝ) :
    listDeletionExpectation q ((bs.map primitiveBlock).flatten) F =
      silentMarkExpectation q bs (fun ys => F (joinPrimitiveMarks ys)) := by
…
```
Mentions: OAI.TraceReconstruction.listDeletionExpectation, OAI.TraceReconstruction.primitiveBlock, OAI.TraceReconstruction.silentMarkExpectation, OAI.TraceReconstruction.joinPrimitiveMarks
def OAI.TraceReconstruction.emittedMarkExpectation line 488
Source documentation
Every emitted mark is counted, including the empty primitive output.
```
def emittedMarkExpectation (q : ℝ) : List Bool → (List PrimitiveMark → ℝ) → ℝ
  | [], F => F []
  | b::bs, F => ∑z : PrimitiveMark, primitiveMarkMass q b z*
      emittedMarkExpectation q bs (fun ys => F (z::ys))
```
Mentions: OAI.TraceReconstruction.PrimitiveMark, OAI.TraceReconstruction.primitiveMarkMass
theorem OAI.TraceReconstruction.emittedMarkExpectation_ofFn line 493
theorem OAI.TraceReconstruction.silentMarkExpectation_mask_mixture line 511
Source documentation
Conditioning the independent erasures on the return count chooses a uniformly random subset of the original block slots.
```
theorem silentMarkExpectation_mask_mixture {n : ℕ} (q : ℝ) (θ : Fin n → Bool)
    (F : List PrimitiveMark → ℝ) :
    silentMarkExpectation q (List.ofFn θ) F=
      ∑a : Mask n, maskWeight (primitiveErasure q) a*
        emittedMarkExpectation q (traceOfMask θ a) F := by
…
```
Mentions: OAI.TraceReconstruction.PrimitiveMark, OAI.TraceReconstruction.silentMarkExpectation, OAI.TraceReconstruction.Mask, OAI.TraceReconstruction.maskWeight, OAI.TraceReconstruction.primitiveErasure, OAI.TraceReconstruction.emittedMarkExpectation, OAI.TraceReconstruction.traceOfMask
def OAI.TraceReconstruction.maskSubset line 536
def OAI.TraceReconstruction.maskSubsetEquiv line 538
theorem OAI.TraceReconstruction.maskWeight_card line 544
theorem OAI.TraceReconstruction.slotAtRank_ofFn line 555
theorem OAI.TraceReconstruction.filtered_finRange_eq_sort line 563
theorem OAI.TraceReconstruction.selected_types_ofFn line 569
theorem OAI.TraceReconstruction.silentMarkExpectation_subset_mixture line 574
def OAI.TraceReconstruction.cardinalSubsetEquiv line 589
theorem OAI.TraceReconstruction.subsetWeight_count_factor line 600
def OAI.TraceReconstruction.conditionalPrimitiveLaw line 607
Source documentation
The literal conditional-list oracle used by the rank coefficients.
```
def conditionalPrimitiveLaw {n l : ℕ} (hl : l ≤ n) (q : ℝ) (hq : q∈Set.Ioo 0 1)
    (θ : Fin n → Bool) : FiniteLaw (Fin l → PrimitiveMark) :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.PrimitiveMark
theorem OAI.TraceReconstruction.silentMarkExpectation_count_mixture line 612
theorem OAI.TraceReconstruction.conditionalPrimitiveLaw_density line 649
Source documentation
Density of the actual uniform-subset primitive oracle, over the ordinary mark product law. This is exactly the channel defined by silent erasures.
```
theorem conditionalPrimitiveLaw_density {n l : ℕ} (hl : l ≤ n)
    {q : ℝ} (hq : q∈Set.Ioo 0 1) (θ : Fin n → Bool) (x : Fin l → PrimitiveMark) :
    (conditionalPrimitiveLaw hl q hq θ).mass x =
      ((primitiveMarkLaw q hq false).product l).mass x *
        averagedDensity (uniformSubsetLaw l (by simpa using hl))
          (fun S v => θ (slotAtRank S v)) (primitiveScore q) x := by
…
```
Mentions: OAI.TraceReconstruction.PrimitiveMark, OAI.TraceReconstruction.conditionalPrimitiveLaw, OAI.TraceReconstruction.primitiveMarkLaw, OAI.TraceReconstruction.averagedDensity, OAI.TraceReconstruction.uniformSubsetLaw, OAI.TraceReconstruction.slotAtRank, OAI.TraceReconstruction.primitiveScore
def OAI.TraceReconstruction.defectTypes line 670
theorem OAI.TraceReconstruction.defectTypes_atRank line 672
theorem OAI.TraceReconstruction.conditionalDefectLaw_density line 677
def OAI.TraceReconstruction.seriesProbabilityLaw line 689
Source documentation
The finite-support law of the hidden motif anchor, not an additional distributional assumption or a changed channel parameter.
```
def seriesProbabilityLaw (π : IntSeries) (hπ : ∀X, 0 ≤ π.coeff X)
    (hπsum : ∑X∈π.coeff.support, π.coeff X=1) : FiniteLaw ↥π.coeff.support where
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.FiniteLaw
def OAI.TraceReconstruction.mixedMotifCoefficient line 695
def OAI.TraceReconstruction.conditionalMotifLaw line 702
theorem OAI.TraceReconstruction.conditionalMotifLaw_density line 710
theorem OAI.TraceReconstruction.mixedMotifCoefficient_rank_difference line 737
def OAI.TraceReconstruction.unchangedPattern line 758
theorem OAI.TraceReconstruction.unchanged_positional_value line 760
theorem OAI.TraceReconstruction.motif_pure_shift_expansion line 769
Source documentation
Comparing a signed displaced motif with the literal centered pure run retains every nonconstant positional pattern, not just odd ones.
```
theorem motif_pure_shift_expansion {r : ℕ} (χ β : Fin r → ℝ)
    (hβ : ∀h, IsMotifValue (χ h) (β h)) (W : (Fin r → Fin 3) → ℝ) :
    W (fun h => motifShift (χ h) (β h) 1)-W (fun _ => 1)=
      ∑ k : Fin r → GapDifference, if k=unchangedPattern r then 0 else
        (∏h, motifDifferenceWeight (χ h) (β h) 1 (k h))*
          (∑a : Fin r → Fin 3, (∏h, positionalWeight (k h) (a h))*W a) := by
…
```
Mentions: OAI.TraceReconstruction.IsMotifValue, OAI.TraceReconstruction.motifShift, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.unchangedPattern, OAI.TraceReconstruction.motifDifferenceWeight, OAI.TraceReconstruction.positionalWeight
theorem OAI.TraceReconstruction.mixed_pure_shift_expansion line 788
theorem OAI.TraceReconstruction.pattern_order_zero line 807
theorem OAI.TraceReconstruction.nonconstant_pattern_linear_or_order_two line 816
theorem OAI.TraceReconstruction.nonconstant_pattern_position line 832
Source documentation
A nonconstant motif pattern always has an actual involved position.
```
theorem nonconstant_pattern_position {r : ℕ} (k : Fin r → GapDifference)
    (hk : k≠unchangedPattern r) : ∃a, k a≠.unchanged := by
…
```
Mentions: OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.unchangedPattern
theorem OAI.TraceReconstruction.clipped_pure_nonlinear_pattern_norm line 838
def OAI.TraceReconstruction.purePatternBound line 863
theorem OAI.TraceReconstruction.clipped_pure_initial_norm line 871
Source documentation
Complete clipped energy, comparing the signed motif to a pure run.
```
theorem clipped_pure_initial_norm {u m l r : ℕ}
    (hm : 32 ≤ m) (hr : 0 < r) (hl : l ≤ u*m)
    (off : Fin m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hsafe : SafeTaggedTuple (periodSlot (u := u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.shiftedTag_center line 905
def OAI.TraceReconstruction.pureRankCoefficient line 911
def OAI.TraceReconstruction.pureTupleKernel line 918
theorem OAI.TraceReconstruction.pureRankCoefficient_tuple_sum line 925
theorem OAI.TraceReconstruction.pureTupleKernel_expansion line 935
def OAI.TraceReconstruction.clippedPureRankCoefficient line 950
theorem OAI.TraceReconstruction.clippedPureRankCoefficient_expansion line 955
theorem OAI.TraceReconstruction.pureTupleKernel_tail line 981
theorem OAI.TraceReconstruction.pureRankCoefficient_tail line 1040
theorem OAI.TraceReconstruction.initial_pure_energy line 1069
def OAI.TraceReconstruction.scaleCoefficient line 1108
theorem OAI.TraceReconstruction.multilinear_scale line 1111
theorem OAI.TraceReconstruction.multilinearEnergy_scale line 1124

theorem OAI.TraceReconstruction.multilinear_moment_scaled line 1137

Source documentation

The exact norm-of-input factor in the conditional leaf expansion.

theorem multilinear_moment_scaled {α : Type*} [Fintype α] (P : FiniteLaw α)
    (Z : α → ℝ) (k : ℕ) (hk : 1 ≤ k) (hcenter : P.expect Z=0)
    {L : ℝ} (hL : 0<L) (hMoment : P.expect (fun a => |Z a|^(2*k))≤L^(2*k))
    (n : ℕ) (A : (Fin n → Bool) → ℝ) :
    (P.product n).expect (fun x => |multilinear A Z x|^(2*k)) ≤
      (multilinearEnergy A ((6*(2*k:ℕ):ℝ)*L))^k := by
…

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

theorem OAI.TraceReconstruction.multilinear_moment_sq_scaled line 1159
theorem OAI.TraceReconstruction.multilinearEnergy_mixture_le line 1175
theorem OAI.TraceReconstruction.multilinearEnergy_sub_le line 1191