OAI/Analysis/FiniteFactor/CrossedProduct/BoundaryEvent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceExclusionWidth line 11

   Source documentation

   The source margin 2K_j/N_s. At s=j it is exactly 2/m_j.

   def sourceExclusionWidth (j : ℕ) (i : SourceCoordinate) : ℝ :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

2. def OAI.FiniteFactor.sourceBoundaryEvent line 14
3. theorem OAI.FiniteFactor.sourceExclusionWidth_current line 19
4. theorem OAI.FiniteFactor.sourceBoundaryEvent_measurable line 24
5. theorem OAI.FiniteFactor.sourceBoundary_floor_zero line 36

   Source documentation

   The actual source margins force zero later-coordinate floors for both signs needed by the finite coefficient bound.

   theorem sourceBoundary_floor_zero (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (j : ℕ) (ω : SourceBiasedSample) (he : ω ∈ sourceBoundaryEvent j)
       (hxc : ∀ i, sourceBiasedEndpoint (fun _ => false) ω i ∈ Set.Ico 0 1)
       (hyc : ∀ i, sourceBiasedEndpoint (fun _ => true) ω i ∈ Set.Ico 0 1)
       (v : ℤ) (hv : 0 ≤ v) (hvK : (v : ℝ) ≤ (sourceStageState j).K) :
       ∀ i : SourceCoordinate, j ≤ i.1 →
         coordinateFloor θ v (sourceBiasedEndpoint (fun _ => false) ω) i = 0 ∧
         coordinateFloor θ (-v) (sourceBiasedEndpoint (fun _ => true) ω) i = 0 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceBiasedSample, OAI.FiniteFactor.sourceBoundaryEvent, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.coordinateFloor