AveragedArithmeticTransfer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Retaining the complex off-diagonal through the outside average

theorem OAI.Ostmann.averaged_arithmetic_transfer line 13

Source documentation

The real-part form must be averaged before taking the norm of the next amplitude. The original outside law may be a subprobability law.

theorem averaged_arithmetic_transfer {Y : Type*} [Fintype Y]
    (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (hmass : ∑ y, μ y ≤ 1)
    (η θ : Y → ℂ) (D : Y → ℝ) (C : ℝ) (hC : 0 ≤ C)
    (hlocal : ∀ y, ‖η y‖ ^ 2 ≤ C * (D y + (θ y).re)) :
    ‖∑ y, (μ y : ℂ) * η y‖ ^ 2 ≤
      C * ((∑ y, μ y * D y) + ‖∑ y, (μ y : ℂ) * θ y‖) := by
…

theorem OAI.Ostmann.normalized_arithmetic_transfer line 37

Source documentation

A concrete harmonic-prior loss bounded by exp(d) gives the normalized transfer inequality used by the iteration theorem.

theorem normalized_arithmetic_transfer (η θ : ℂ) (D C d : ℝ)
    (hD : 0 ≤ D) (hC : C ≤ Real.exp d)
    (htransfer : ‖η‖ ^ 2 ≤ C * (D + ‖θ‖)) :
    Real.exp (-d) * ‖η‖ ^ 2 ≤ D + ‖θ‖ := by
…