OAI/NumberTheory/TwoPoint/Bounds/ActualCodeAssignments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.actualSlotPrime_mem_tuplePool line 15
2. lemma OAI.TwoPointCorrelations.actualSlotPrime_mem_paddingPool line 22
3. lemma OAI.TwoPointCorrelations.actualPrimeSlotData_prime_image line 29
4. lemma OAI.TwoPointCorrelations.actualPrimeSlot_support line 42
5. theorem OAI.TwoPointCorrelations.actual_code_reciprocal_weight line 63

   Source documentation

   The encoded assignment pays exactly one reciprocal per distinct prime.

   theorem actual_code_reciprocal_weight (w : Fin R → SignedStep)
       (ht : ∀ i, (w i).tuple ≠ 0) (hq : ∀ i, (w i).padding ≠ 0) :
       (∏ z : (actualPrimeSlotData w).code.usedClasses,
         ((actualPrimeSlotData w).prime z.val : ℝ)⁻¹) =
         ∏ p ∈ wordDivisorPrimeSupport (List.ofFn w), (p : ℝ)⁻¹ := by
   …

   Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.actualPrimeSlotData, OAI.TwoPointCorrelations.wordDivisorPrimeSupport

6. theorem OAI.TwoPointCorrelations.actual_code_pool_assignments line 73

   Source documentation

   Actual tuple and padding classes inhabit their separate numerical pools.

   theorem actual_code_pool_assignments (w : Fin R → SignedStep) (P Q : Finset ℕ)
       (hP : ∀ i, (w i).tuple.primeFactors ⊆ P)
       (hQ : ∀ i, (w i).padding.primeFactors ⊆ Q) :
       ∃ a : (actualPrimeSlotData w).code.tupleClasses → P,
         ∃ b : {z : (actualPrimeSlotData w).code.usedClasses //
           z ∉ (actualPrimeSlotData w).code.tupleClasses} → Q,
         joinCoordinates (actualPrimeSlotData w).code.tupleClasses
           (fun z => (a z).val) (fun z => (b z).val) =
             fun z => (actualPrimeSlotData w).prime z.val := by
   …

   Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.actualPrimeSlotData, OAI.TwoPointCorrelations.joinCoordinates