MixedBulkSymmetrization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Symmetrization of the original mixed law, with bad pairs paid by energy

def OAI.Ostmann.mixedBulkSymmetrize line 11
theorem OAI.Ostmann.mixedExternalAverage_weighted_square_permute line 17

theorem OAI.Ostmann.mixedBulkSymmetrize_energy_bound line 34

Source documentation

The ordinary diagonal energy controls every bad pair. Only good relative permutations use the signed arithmetic correlation estimate.

theorem mixedBulkSymmetrize_energy_bound {B A : Type*} [Fintype B] [Fintype A]
    (n m : ℕ) (hm : 1 ≤ m) (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (ν : B → A → ℝ) (hν : ∀ b a, 0 ≤ ν b a)
    (hidentical : ∀ j k, ν (slot j) = ν (slot k))
    (N : ℕ) (u v r w center : ℝ)
    (F : ℤ → (B → A) → ℝ → ℝ → ℂ) (W : ℤ → (B → A) → ℝ → ℝ → ℝ)
    (hW : ∀ s y x z, 0 ≤ W s y x z)
    (hinv : ∀ e s y x z, W s (selectedBulkSample slot e y) x z = W s y x z)
    (D E : ℝ) (hD : 0 ≤ D) (hE : 0 ≤ E)
    (hdiag : (mixedExternalAverage ν N u v r w center
      (fun s y x z => (‖F s y x z‖ ^ 2 : ℂ) * W s y x z)).re ≤ D)
    (hgood : ∀ e : Equiv.Perm (TreeLeafIndex n × Fin m),
…

Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.selectedBulkSample, OAI.Ostmann.mixedExternalAverage