BadEvents.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.CouplingParameters.eligible line 12
instance OAI.FiniteFactor.CouplingParameters.eligible_decidable line 14
def OAI.FiniteFactor.CouplingParameters.eligibleIndices line 18
theorem OAI.FiniteFactor.CouplingParameters.eligible_measurable line 21
theorem OAI.FiniteFactor.CouplingParameters.eligible_count_measurable line 26
def OAI.FiniteFactor.CouplingParameters.badHalfEvent line 38
Source documentation
A measurable half of the noncrossing event, with the eligibility count read from the conditioning vector. Taking right=false or right=true gives the two orientations used in the contradiction.
```
def badHalfEvent {ι : Type*} (right : ι → Bool) (u : ι → ℝ) (I : Finset ι) (q : ℝ) :
    Set ((ι → ℝ) × (ι → ℝ)) :=
…
```
theorem OAI.FiniteFactor.CouplingParameters.badHalfEvent_measurable line 43
theorem OAI.FiniteFactor.CouplingParameters.badHalfEvent_section line 61
theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_badHalf_bound line 75
theorem OAI.FiniteFactor.CouplingParameters.vectorEndpoint_unitCube line 104

theorem OAI.FiniteFactor.CouplingParameters.badHalf_condExp_bound line 118

Source documentation

Actual conditional bound for each oriented bad event, ready for the countably infinite masked-sum theorem. No conditional-independence assumption or posterior bound is an input.

theorem badHalf_condExp_bound {ι : Type*} [Countable ι]
    (p : ι → CouplingParameters) (right : ι → Bool) (w : ι → Fin 2)
    (u : ι → ℝ) (I : Finset ι) (q m ρ L : ℝ)
    (hu : ∀ i ∈ I, (p i).width (w i) ≤ u i ∧ u i ≤ 1-(p i).width (w i))
    (hρ : ∀ i ∈ I, (p i).rho (w i) = ρ)
    (hρ0 : 0 ≤ ρ) (hq : m/20 ≤ q) (hL : L ≤ m*ρ) :
    ∀ᵐ ω ∂vectorCoupling p,
      (vectorCoupling p)[
        (fun ω => (badHalfEvent right u I q).indicator (fun _ => (1 : ℝ))
          (vectorEndpoint right ω, vectorEndpoint (fun i => !right i) ω)) |
        (inferInstance : MeasurableSpace (ι → ℝ)).comap (vectorEndpoint right)] ω ≤ Real.exp (-L/400) := by
…

Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.rho, OAI.FiniteFactor.CouplingParameters.vectorCoupling, OAI.FiniteFactor.CouplingParameters.badHalfEvent, OAI.FiniteFactor.CouplingParameters.vectorEndpoint

theorem OAI.FiniteFactor.CouplingParameters.noncrossing_eligible_complement line 138
Source documentation
On ordered noncrossing pairs, the two eligibility counts are complementary. Thus the strict second half of the source bad event lies in the reverse badHalfEvent; using a weak inequality there only enlarges that event.
```
theorem noncrossing_eligible_complement {ι : Type*} (x y u : ι → ℝ) (I : Finset ι)
    (hxy : ∀ i ∈ I, x i ≤ y i) (hn : ∀ i ∈ I, ¬(x i < u i ∧ u i ≤ y i)) :
    (eligibleIndices (fun _ => false) x u I).card +
      (eligibleIndices (fun _ => true) y u I).card = I.card := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters.eligibleIndices
theorem OAI.FiniteFactor.CouplingParameters.second_bad_half_in_reverse line 155
Source documentation
Exact source second-half event is contained in the reverse event whose conditional estimate was proved above. All coordinates in I are accounted for.
```
theorem second_bad_half_in_reverse {ι : Type*} (x y u : ι → ℝ) (I : Finset ι)
    (hxy : ∀ i ∈ I, x i ≤ y i)
    (hn : ∀ i ∈ I, ¬(x i < u i ∧ u i ≤ y i))
    (hcount : ((eligibleIndices (fun _ => false) x u I).card : ℝ) < (I.card : ℝ)/2) :
    (y,x) ∈ badHalfEvent (fun _ => true) u I I.card := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters.eligibleIndices, OAI.FiniteFactor.CouplingParameters.badHalfEvent
theorem OAI.FiniteFactor.CouplingParameters.vectorCoupling_ordered line 170
Source documentation
The pointwise orderedness needed for the complementary-event argument is itself a theorem about the actual full augmented law.
```
theorem vectorCoupling_ordered {ι : Type*} [Countable ι] (p : ι → CouplingParameters) :
    vectorCoupling p {ω | ∀ i, (ω i).2.1 ≤ (ω i).2.2} = 1 := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorCoupling