OAI/Analysis/FiniteFactor/CrossedProduct/EventLossAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceCurrentFuture_boundary line 13

   Source documentation

   Current and future exclusions together give exactly the source boundary.

   theorem sourceCurrentFuture_boundary (j : ℕ) (ω : SourceBiasedSample)
       (hc : ω ∈ sourceCurrentTaggedEvent j) (hf : ω ∈ sourceFutureBoundaryEvent j) :
       ω ∈ sourceBoundaryEvent j := by
   …

   Mentions: OAI.FiniteFactor.SourceBiasedSample, OAI.FiniteFactor.sourceCurrentTaggedEvent, OAI.FiniteFactor.sourceFutureBoundaryEvent, OAI.FiniteFactor.sourceBoundaryEvent

2. def OAI.FiniteFactor.sourceDiagonalLossSet line 27
3. theorem OAI.FiniteFactor.sourceProjectionEvent_mass_losses line 34

   Source documentation

   No independence is used between the current block and the three losses.

   theorem sourceProjectionEvent_mass_losses
       (p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) (j : ℕ) :
       Real.exp (-82) ≤ (sourceBiasedLaw j).real (sourceProjectionEvent p j) +
         (sourceBiasedLaw j).real (sourceFutureBoundaryEvent j)ᶜ +
         (sourceBiasedLaw j).real (sourceDiagonalLossSet p j false) +
         (sourceBiasedLaw j).real (sourceDiagonalLossSet p j true) := by
   …

   Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceProjectionEvent, OAI.FiniteFactor.sourceFutureBoundaryEvent, OAI.FiniteFactor.sourceDiagonalLossSet