BackwardSwitchProbability.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Probability of retaining every intermediate sheet

def OAI.PolycyclicRecognition.survivingSwitchProbability line 18

Source documentation

Iterate the actual independent pairs of increment samples, killing a path at its first exit from the prescribed next set.

def survivingSwitchProbability (σ : ℕ → Measure G) (S : ℕ → Set G) :
    ℕ → ℕ → G → ℝ≥0∞
  | _, 0, _ => 1
  | n, k + 1, x => ∫⁻ s₁, ∫⁻ s₂,
      (S (n + 1)).indicator (survivingSwitchProbability σ S (n + 1) k)
        (x * s₁ * s₂⁻¹) ∂σ n ∂σ n

/-- The product of the successive transition thresholds, in the same
recursive order as the independent sampling. -/

def OAI.PolycyclicRecognition.switchThresholdProduct line 27
Source documentation
The product of the successive transition thresholds, in the same recursive order as the independent sampling.
```
def switchThresholdProduct (τ : ℕ → ℝ≥0) : ℕ → ℕ → ℝ≥0∞
  | _, 0 => 1
  | n, k + 1 => τ n * switchThresholdProduct τ (n + 1) k
```
theorem OAI.PolycyclicRecognition.switchThresholdProduct_ne_top line 31
theorem OAI.PolycyclicRecognition.switchThresholdProduct_pos line 37
theorem OAI.PolycyclicRecognition.survivingSwitchProbability_le_one line 47
theorem OAI.PolycyclicRecognition.measurable_survivingSwitchProbability line 65
theorem OAI.PolycyclicRecognition.switchThresholdProduct_le_survival line 82
Source documentation
Independent sampling multiplies the conditional return bounds. The sets may differ at each stage, which is essential for backward recurrence.
```
theorem switchThresholdProduct_le_survival
    (σ : ℕ → Measure G) (S : ℕ → Set G) (τ : ℕ → ℝ≥0)
    (n k : ℕ)
    (hreturn : ∀ j, j < n + k → ∀ x ∈ S j,
      (τ j : ℝ≥0∞) ≤ twoSampleReturn (σ j) (S (j + 1)) x)
    {x : G} (hx : x ∈ S n) :
    switchThresholdProduct τ n k ≤ survivingSwitchProbability σ S n k x := by
…
```
Mentions: OAI.PolycyclicRecognition.twoSampleReturn, OAI.PolycyclicRecognition.switchThresholdProduct, OAI.PolycyclicRecognition.survivingSwitchProbability