OAI/NumberTheory/Ostmann/Construction/TwoCoordinatePrior.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.twoCoordinateAssignment line 12
2. theorem OAI.Ostmann.twoCoordinateAssignment_short line 16
3. theorem OAI.Ostmann.twoCoordinateAssignment_long line 23
4. theorem OAI.Ostmann.twoCoordinateAssignment_other line 30
5. theorem OAI.Ostmann.twoCoordinateAssignment_update_long line 37
6. def OAI.Ostmann.twoCoordinateEquiv line 51
7. theorem OAI.Ostmann.productPrior_twoCoordinates line 67
8. theorem OAI.Ostmann.sum_productPrior_twoCoordinates line 78
9. theorem OAI.Ostmann.original_prior_twoCoordinate_bound line 102

   Source documentation

   The section bound is averaged under every remaining original coordinate prior. All range, distinctness and history restrictions stay inside F.

   theorem original_prior_twoCoordinate_bound {V A : Type*} [Fintype V] [Fintype A]
       (a b : V) (hab : a ≠ b) (μ : V → A → ℝ)
       (hμ : ∀ v x, 0 ≤ μ v x) (hmass : ∀ v, ∑ x, μ v x ≤ 1)
       (F : (V → A) → ℂ) (δ : ℝ) (hδ : 0 ≤ δ)
       (hsection : ∀ outside : OtherVertices a b → A,
         ‖∑ q, (μ a q : ℂ) * ∑ p, (μ b p : ℂ) *
           F (twoCoordinateAssignment a b hab outside q p)‖ ≤ δ) :
       ‖∑ x, ((∏ v, μ v (x v) : ℝ) : ℂ) * F x‖ ≤ δ := by
   …

   Mentions: OAI.Ostmann.OtherVertices, OAI.Ostmann.twoCoordinateAssignment