OAI/Probability/CubeShuffle/ModifiedKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.PairRouting.tupleProbability_row_sum line 10
2. lemma OAI.CubeShuffle.PairRouting.tupleProbability_inverse line 24
3. lemma OAI.CubeShuffle.PairRouting.tupleProbability_equiv line 40
4. lemma OAI.CubeShuffle.PairRouting.tupleProbability_symmetric line 45
5. lemma OAI.CubeShuffle.palindromePerm_reverse line 55
6. lemma OAI.CubeShuffle.palindrome_kernel_symmetric line 60
7. theorem OAI.CubeShuffle.palindrome_density_transfer line 69

   Source documentation

   The actual palindrome density estimate combined with the proved finite Schur/Bessel transfer. The family is an arbitrary orthonormal family in the literal tuple space, not an assumed representation of the desired theorem.

   theorem palindrome_density_transfer (d : ℕ) {ι I : Type*} [Fintype ι] [Fintype I]
       [Nonempty I] (e₀ : ι ↪ Card d) (hk : 0 < Fintype.card ι)
       (v : I → EuclideanSpace ℂ (ι ↪ Card d)) (hv : Orthonormal ℂ v)
       (μ : ℝ) (hvμ : ∀ i, μ ≤ ‖DensityTransfer.applyKernel
         (fun e f : ι ↪ Card d => PairRouting.tupleProbability (palindromePerm d) e f) (v i)‖)
       (z : ℝ) (hz : 0 < z) :
       μ ≤ Real.exp (densityConstant*Fintype.card ι*
         ((Fintype.card ι:ℝ)/(2:ℝ)^d)^(1/512:ℝ))*z^(-(1/1000:ℝ))+
         Real.sqrt (z/(Fintype.card I:ℝ)) := by
   …

   Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.DensityTransfer.applyKernel, OAI.CubeShuffle.PairRouting.tupleProbability, OAI.CubeShuffle.palindromePerm, OAI.CubeShuffle.densityConstant

8. def OAI.CubeShuffle.modifiedReverseCoins line 93

   Source documentation

   A measure-preserving reversal of the actual modified coin experiment. At a leaf the redundant output butterfly is kept, while its uniform seed is inverted and conjugated. At higher nodes the two outer fair fields are swapped.

   noncomputable def modifiedReverseCoins (L : ℕ) : (r : ℕ) → ModifiedCoins L r → ModifiedCoins L r
     | 0, ω => ((fun u => butterflyPerm L (decodeButterfly L ω.2.1) * (ω.1 u)⁻¹ *
         butterflyPerm L (decodeButterfly L ω.2.1)),ω.2)
     | r+1, ω =>
         let z := modifiedStepEquiv L r ω
   …

   Mentions: OAI.CubeShuffle.ModifiedCoins, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.modifiedStepEquiv

9. lemma OAI.CubeShuffle.modifiedReverseCoins_involutive line 101
10. def OAI.CubeShuffle.modifiedReverseEquiv line 117
11. lemma OAI.CubeShuffle.modifiedPerm_reverse line 123
12. lemma OAI.CubeShuffle.modified_kernel_symmetric line 144