ExpandedPaths.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedTreewidthL1.ExpandedChain.past line 13
lemma OAI.BoundedTreewidthL1.ExpandedChain.past_bounds line 17
lemma OAI.BoundedTreewidthL1.ExpandedChain.sum_fiber_mul line 25

lemma OAI.BoundedTreewidthL1.ExpandedChain.weighted_terminal line 36

Source documentation

Conditional past means in the actual finite product law, not an assumed Markov response. This identity includes all zero-mass states.

lemma weighted_terminal (μ : ℕ → A → ℝ) (Q : ℕ → A → A → ℝ)
    (hQ : ∀ n, IsCoupling (μ n) (μ (n+1)) (Q n)) (f : A → ℝ) (n : ℕ) (b : A) :
    (∑ x : MarkovProduct.History (fun _ => A) n,
      if x (Fin.last n) = b then
        MarkovProduct.weight (fun _ => A) (μ 0) (MarkovProduct.couplingKernel (fun _ => A) μ Q) n x * f (x 0)
      else 0) = μ n b * past μ Q f n b := by
…

Mentions: OAI.BoundedTreewidthL1.MarkovProduct.History, OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel, OAI.BoundedTreewidthL1.ExpandedChain.past

theorem OAI.BoundedTreewidthL1.ExpandedChain.endpoint_defect line 83
Source documentation
Separation of endpoint labels in the genuine product density is precisely its conditional-predictor defect. The identity holds for all bounded or unbounded real endpoint observables; bounds are needed only for the subsequent tests.
```
theorem endpoint_defect (μ : ℕ → A → ℝ) (Q : ℕ → A → A → ℝ)
    (hQ : ∀ n, IsCoupling (μ n) (μ (n+1)) (Q n)) (f g : A → ℝ) (n : ℕ) :
    (∑ x : MarkovProduct.History (fun _ => A) n,
      MarkovProduct.weight (fun _ => A) (μ 0) (MarkovProduct.couplingKernel (fun _ => A) μ Q) n x *
        (f (x 0) + g (x (Fin.last n)) - 2*f (x 0)*g (x (Fin.last n)))) =
      defect (μ n) g (past μ Q f n) := by
…
```
Mentions: OAI.BoundedTreewidthL1.MarkovProduct.History, OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel, OAI.BoundedTreewidthL1.ExpandedChain.past
lemma OAI.BoundedTreewidthL1.ExpandedChain.response_past line 124

theorem OAI.BoundedTreewidthL1.ExpandedChain.endpoint_defect_at line 138

Source documentation

One may test at ANY interior location: past and future are the honest conditional responses of the already constructed product law.

theorem endpoint_defect_at (μ : ℕ → A → ℝ) (Q : ℕ → A → A → ℝ)
    (hQ : ∀ n, IsCoupling (μ n) (μ (n+1)) (Q n)) (f g : A → ℝ) (t n : ℕ) (ht : t ≤ n) :
    (∑ x : MarkovProduct.History (fun _ => A) n,
      MarkovProduct.weight (fun _ => A) (μ 0) (MarkovProduct.couplingKernel (fun _ => A) μ Q) n x *
        (f (x 0) + g (x (Fin.last n)) - 2*f (x 0)*g (x (Fin.last n)))) =
      defect (μ t) (response μ Q t (n-t) g) (past μ Q f t) := by
…

Mentions: OAI.BoundedTreewidthL1.MarkovProduct.History, OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel, OAI.BoundedTreewidthL1.ExpandedChain.past

theorem OAI.BoundedTreewidthL1.ReservedSuffix.response_restrict_local line 155

Source documentation

Local version: the arbitrary past of the path is immaterial. Only the true reserved suffix edges are prescribed.

theorem response_restrict_local (M : ℝ) (F : ℕ → ι → V → ℝ) (P : ℕ → Finset V)
    (fresh₁ fresh₂ : ℕ → ι) (C : ℕ → Finset ι)
    (Q : ℕ → State ι V → State ι V → ℝ)
    (t n : ℕ) (r : ι) (G : V → ℝ)
    (hQ : ∀ s, t ≤ s → s < t+n → Q s = kernels M F P fresh₁ fresh₂ C s)
    (hret : ∀ s, t ≤ s → s < t+n → ∀ r ∈ C s, F s r = F (s+1) r)
    (htrace : ∀ s, t ≤ s → s < t+n →
      particleTrace M (F s) (P (s+1)) = particleTrace M (F (s+1)) (P (s+1)))
    (hfixed : ∀ s, t ≤ s → s ≤ t+n → F s r = G)
    (hkeep : ∀ s, t ≤ s → s < t+n → r ∈ C s ∧ r ≠ fresh₁ s ∧ r ≠ fresh₂ s)
    (z : V) (a : OrderedReservation.Carrier M G) :
    response (fun s => weight M (F s)) Q t n
…

Mentions: OAI.BoundedTreewidthL1.ReservedSuffix.kernels, OAI.BoundedTreewidthL1.particleTrace, OAI.BoundedTreewidthL1.OrderedReservation.Carrier

lemma OAI.BoundedTreewidthL1.ReservedSuffix.ordered_mean line 194
lemma OAI.BoundedTreewidthL1.ReservedSuffix.incoming_response_restrict line 232
def OAI.BoundedTreewidthL1.ExpandedPathTests.distance line 265
lemma OAI.BoundedTreewidthL1.ExpandedPathTests.distance_at line 272

theorem OAI.BoundedTreewidthL1.ExpandedPathTests.height_test line 292

Source documentation

Height test for the ACTUAL arbitrarily prefixed product path. All suffix transport and both past/future responses are derived from its couplings.

theorem height_test (M : ℝ) (hM : 0 ≤ M) (F : ℕ → ι → V → ℝ) (P : ℕ → Finset V)
    (fresh₁ fresh₂ : ℕ → ι) (C : ℕ → Finset ι)
    (Q : ℕ → State ι V → State ι V → ℝ)
    (hQ : ∀ s, IsCoupling (weight M (F s)) (weight M (F (s+1))) (Q s))
    (t n : ℕ) (r : ι)
    (hEq : ∀ s, t ≤ s → s < t+1+n → Q s = kernels M F P fresh₁ fresh₂ C s)
    (hret : ∀ s, t ≤ s → s < t+1+n → ∀ r ∈ C s, F s r = F (s+1) r)
    (htrace : ∀ s, t ≤ s → s < t+1+n →
      particleTrace M (F s) (P (s+1)) = particleTrace M (F (s+1)) (P (s+1)))
    (hfixed : ∀ s, t ≤ s → s ≤ t+1+n → F s r = F t r)
    (hkeep : ∀ s, t ≤ s → s < t+1+n → r ∈ C s ∧ r ≠ fresh₁ s ∧ r ≠ fresh₂ s)
    (hF : ∀ v, -M ≤ F t r v ∧ F t r v ≤ M) (y z : V)
…

Mentions: OAI.BoundedTreewidthL1.particleTrace

theorem OAI.BoundedTreewidthL1.ExpandedPathTests.launch_test line 330

Source documentation

Fresh-pair test on the actual product law with an arbitrary prefix.

theorem launch_test (M : ℝ) (hM : 0 ≤ M) (F : ℕ → ι → V → ℝ) (P : ℕ → Finset V)
    (fresh₁ fresh₂ : ℕ → ι) (C : ℕ → Finset ι)
    (Q : ℕ → State ι V → State ι V → ℝ)
    (hQ : ∀ s, IsCoupling (weight M (F s)) (weight M (F (s+1))) (Q s))
    (t n : ℕ) (hij : fresh₁ t ≠ fresh₂ t)
    (hbag : ∀ v ∈ P t, F t (fresh₁ t) v = F t (fresh₂ t) v)
    (hEq : ∀ s, t ≤ s → s < t+1+n → Q s = kernels M F P fresh₁ fresh₂ C s)
    (hret : ∀ s, t ≤ s → s < t+1+n → ∀ r ∈ C s, F s r = F (s+1) r)
    (htrace : ∀ s, t ≤ s → s < t+1+n →
      particleTrace M (F s) (P (s+1)) = particleTrace M (F (s+1)) (P (s+1)))
    (hfixed : ∀ r ∈ ({fresh₁ t, fresh₂ t} : Finset ι),
      ∀ s, t ≤ s → s ≤ t+1+n → F s r = F t r)
…

Mentions: OAI.BoundedTreewidthL1.particleTrace