AssignedBadEvents.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.FiniteFactor.SourcePhaseAssignment line 13
Source documentation
A deterministic source phase assignment, chosen from the fixed angles.
```
structure SourcePhaseAssignment (θ : SourceCoordinate → ℝ) (j : ℕ) (k : ℤ) where
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate
def OAI.FiniteFactor.sourceChosenAssignment line 24
def OAI.FiniteFactor.SourcePhaseAssignment.badEvent line 35
theorem OAI.FiniteFactor.SourcePhaseAssignment.badEvent_measurable line 40
theorem OAI.FiniteFactor.SourcePhaseAssignment.badEvent_condExp line 47
Source documentation
Both conditional estimates use the actual full-vector posterior and the constructed numerical budget. The assignment has no sample argument.
```
theorem badEvent_condExp (a : SourcePhaseAssignment θ j k) (b : Bool) :
    ∀ᵐ ω ∂sourceBiasedLaw j,
      (sourceBiasedLaw j)[(a.badEvent b).indicator (fun _ => (1 : ℝ)) |
        (inferInstance : MeasurableSpace (SourceCoordinate → ℝ)).comap
          (sourceBiasedEndpoint (fun _ => b))] ω ≤ Real.exp (-(sourceStage j).L/400) := by
…
```
Mentions: OAI.FiniteFactor.SourcePhaseAssignment, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceStage
theorem OAI.FiniteFactor.SourcePhaseAssignment.attenuation_or_bad line 78
Source documentation
At an assigned index, failure of both oriented bad events forces an actual floor crossing, hence the original uncapped ratio is attenuated.
```
theorem attenuation_or_bad (hθ : SourceAngles θ) (a : SourcePhaseAssignment θ j k) :
    ∀ᵐ ω ∂sourceBiasedLaw j,
      sourceCocycle θ sourceLogWeight k (sourceBiasedEndpoint (fun _ => true) ω) /
        sourceCocycle θ sourceLogWeight k (sourceBiasedEndpoint (fun _ => false) ω) ≤
          Real.exp (-(sourceStage j).L) ∨ ω ∈ a.badEvent false ∨ ω ∈ a.badEvent true := by
…
```
Mentions: OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourcePhaseAssignment, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceStage