OAI/NumberTheory/Ostmann/Construction/FinalActualPrior.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.finalBulkPrior line 11
2. def OAI.Ostmann.finalSamplePerm line 15
3. def OAI.Ostmann.finalReassignedValue line 19
4. theorem OAI.Ostmann.finalBulkPrior_preserved line 24
5. theorem OAI.Ostmann.finalBulkPrior_nonneg line 30
6. theorem OAI.Ostmann.finalBulkPrior_mass line 35
7. theorem OAI.Ostmann.finalReassignedValue_mean line 43

   Source documentation

   All support conditions belong to F; no conditional sampling law is used.

   theorem finalReassignedValue_mean {Y A : Type*} [Fintype Y] [Fintype A] {n m : ℕ}
       (ν : Y → ℝ) (μ : A → ℝ)
       (F : (Y × ((ParityPathSum n × Fin m) → A)) → ℂ)
       (e : FinalParityReassignments n m) :
       (∑ x, (finalBulkPrior n m ν μ x : ℂ) * finalReassignedValue F e x) =
         ∑ x, (finalBulkPrior n m ν μ x : ℂ) * F x := by
   …

   Mentions: OAI.Ostmann.ParityPathSum, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.finalBulkPrior, OAI.Ostmann.finalReassignedValue

8. theorem OAI.Ostmann.finalReassignedValue_energy line 54

   Source documentation

   The diagonal norm has the same original prior after reassignment.

   theorem finalReassignedValue_energy {Y A : Type*} [Fintype Y] [Fintype A] {n m : ℕ}
       (ν : Y → ℝ) (μ : A → ℝ)
       (F : (Y × ((ParityPathSum n × Fin m) → A)) → ℂ)
       (e : FinalParityReassignments n m) :
       (∑ x, finalBulkPrior n m ν μ x * ‖finalReassignedValue F e x‖ ^ 2) =
         ∑ x, finalBulkPrior n m ν μ x * ‖F x‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.ParityPathSum, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.finalBulkPrior, OAI.Ostmann.finalReassignedValue

9. theorem OAI.Ostmann.final_actual_prior_comparison line 64