MatchedDiagonalEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Retaining one branch's original prior in the matched diagonal

theorem OAI.Ostmann.matched_energy_point line 12

theorem OAI.Ostmann.matched_diagonal_energy line 22

Source documentation

The other branch's point weight is bounded only on simultaneous support. Each resulting square retains its own original sampling law.

theorem matched_diagonal_energy {A B : Type*} [Fintype A] [Fintype B]
    (e : A ≃ B) (μ : A → ℝ) (ν : B → ℝ) (W : A → ℂ) (Z : B → ℂ)
    (θ : A → ℂ) (A₀ : ℝ) (hA₀ : 0 ≤ A₀)
    (hμ : ∀ a, 0 ≤ μ a) (hν : ∀ b, 0 ≤ ν b) (hθ : ∀ a, ‖θ a‖ ≤ 1)
    (hpoint : ∀ a, W a ≠ 0 → Z (e a) ≠ 0 → μ a ≤ A₀ ∧ ν (e a) ≤ A₀) :
    ‖∑ a, ((μ a * ν (e a) : ℝ) : ℂ) * W a * conj (Z (e a)) * θ a‖ ≤
      A₀ / 2 * ((∑ a, μ a * ‖W a‖ ^ 2) + ∑ b, ν b * ‖Z b‖ ^ 2) := by
…

theorem OAI.Ostmann.external_pivot_normalization line 58

Source documentation

The external-integer count is canceled only after extracting the counterpart's reciprocal scale.

theorem external_pivot_normalization {P : Type*} [Fintype P]
    (F : P → ℂ) (C E T Δ κ : ℝ) (hC : 0 ≤ C) (hE : 0 ≤ E)
    (hcard : (Fintype.card P : ℝ) ≤ Real.exp (T + κ))
    (hF : ∀ p, ‖F p‖ ≤ C * Real.exp (-(T + Δ)) * E) :
    ‖∑ p, F p‖ ≤ C * Real.exp (κ - Δ) * E := by
…