TransferCauchy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite Cauchy--Schwarz step in the history transfer

theorem OAI.Ostmann.complex_pairing_sq_le line 12
theorem OAI.Ostmann.probability_weighted_norm_sq_le line 22

theorem OAI.Ostmann.finite_transfer_row_bound line 42

Source documentation

Each row can have its own modulus and hence its own finite index type. The outer laws remain the original probability measures.

theorem finite_transfer_row_bound {A : Type*} [Fintype A] {T : A → Type*}
    [∀ a, Fintype (T a)] (μ : A → ℝ) (hμ : ∀ a, 0 ≤ μ a) (hmass : ∑ a, μ a = 1)
    (row coefficient : ∀ a, T a → ℂ) (M : A → ℝ)
    (hrow : ∀ a, (∑ t, ‖row a t‖ ^ 2) ≤ M a) :
    ‖∑ a, (μ a : ℂ) * ∑ t, row a t * coefficient a t‖ ^ 2 ≤
      ∑ a, μ a * (M a * ∑ t, ‖coefficient a t‖ ^ 2) := by
…