OAI/Probability/CubeShuffle/FiniteKernel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.DensityTransfer.applyKernel line 9
2. lemma OAI.CubeShuffle.DensityTransfer.applyKernel_apply line 13
3. lemma OAI.CubeShuffle.DensityTransfer.applyKernel_add line 17
4. lemma OAI.CubeShuffle.DensityTransfer.kernel_component_sq line 24
5. lemma OAI.CubeShuffle.DensityTransfer.schur_bound line 39

   Source documentation

   The finite Schur test, proved directly with the actual row/column sums.

   lemma schur_bound {X : Type*} [Fintype X] (P : X → X → ℝ)
       (hP : ∀ x y, 0 ≤ P x y) (δ : ℝ) (hδ : 0 ≤ δ)
       (hrow : ∀ x, ∑ y, P x y ≤ δ) (hcol : ∀ y, ∑ x, P x y ≤ δ)
       (v : EuclideanSpace ℂ X) : ‖applyKernel P v‖ ≤ δ*‖v‖ := by
   …

   Mentions: OAI.CubeShuffle.DensityTransfer.applyKernel

6. lemma OAI.CubeShuffle.DensityTransfer.hilbert_schmidt_family line 68

   Source documentation

   Bessel's inequality controls the total stretch of any orthonormal family by the squared Hilbert--Schmidt norm of the finite real kernel.

   lemma hilbert_schmidt_family {X I : Type*} [Fintype X] [Fintype I]
       (P : X → X → ℝ) (v : I → EuclideanSpace ℂ X) (hv : Orthonormal ℂ v) :
       (∑ i, ‖applyKernel P (v i)‖^2) ≤ ∑ x, ∑ y, (P x y)^2 := by
   …

   Mentions: OAI.CubeShuffle.DensityTransfer.applyKernel

7. lemma OAI.CubeShuffle.DensityTransfer.tail_density_pointwise line 98
8. lemma OAI.CubeShuffle.DensityTransfer.tail_density_mean line 107
9. def OAI.CubeShuffle.DensityTransfer.tailKernel line 113
10. def OAI.CubeShuffle.DensityTransfer.headKernel line 116
11. lemma OAI.CubeShuffle.DensityTransfer.tail_add_head line 119
12. lemma OAI.CubeShuffle.DensityTransfer.tailKernel_nonneg line 125
13. lemma OAI.CubeShuffle.DensityTransfer.tailKernel_row line 130
14. lemma OAI.CubeShuffle.DensityTransfer.tailKernel_schur line 151
15. lemma OAI.CubeShuffle.DensityTransfer.headKernel_hs line 166
16. theorem OAI.CubeShuffle.DensityTransfer.multiplicity_amplification line 197

    Source documentation

    Source FAC.7: multiplicity amplification in a finite symmetric kernel. The orthonormal family is the exact linear-algebra meaning of the m equivalent maximizing singular vectors; no spectral producer for the shuffle is assumed.

    theorem multiplicity_amplification {X I : Type*} [Fintype X] [Nonempty X]
        [Fintype I] [Nonempty I] (P : X → X → ℝ)
        (hP : ∀ x y, 0 ≤ P x y) (hsym : ∀ x y, P x y = P y x)
        (hrow : ∀ x, ∑ y, P x y = 1) (a z M : ℝ) (ha : 0 ≤ a) (hz : 0 < z) (hM0 : 0 ≤ M)
        (hM : ∀ x, finiteMean (fun y => ((Fintype.card X:ℝ)*P x y)^(1+a)) ≤ M)
        (v : I → EuclideanSpace ℂ X) (hv : Orthonormal ℂ v)
        (μ : ℝ) (hvμ : ∀ i, μ ≤ ‖applyKernel P (v i)‖) :
        μ ≤ M*z^(-a)+Real.sqrt (z/(Fintype.card I:ℝ)) := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.DensityTransfer.applyKernel