CobagNoise.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedTreewidthL1.TreeParticles.origin line 21
Source documentation
The discrete launch location depends only on the rooted decomposition and active keys. In particular it does not consult any preparatory randomness.
```
noncomputable def origin (R : RootedForest I) (A : I → Finset J) (root : I) : I → J → I :=
…
```
Mentions: OAI.BoundedTreewidthL1.RootedForest
lemma OAI.BoundedTreewidthL1.TreeParticles.origin_eq line 24
lemma OAI.BoundedTreewidthL1.TreeParticles.origin_fresh line 30
lemma OAI.BoundedTreewidthL1.TreeParticles.origin_transport line 46
lemma OAI.BoundedTreewidthL1.TreeParticles.two_particle_difference line 71

theorem OAI.BoundedTreewidthL1.TreeParticles.origin_particle_gap line 90

Source documentation

The actual active pair at any descendant supplies the original launch separation. The origin is deterministic, so no conditioning on the particle scheduler or sampled coefficients is required.

theorem origin_particle_gap (R : RootedForest I) (root : I) (bag : I → Finset V)
    (A : I → Finset J) (k q : ℕ) (hbag : ∀ i, (bag i).card ≤ k)
    (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q + k.factorial + 2)
    (d : V → V → ℝ) (L H Δ : ℝ) (hH : 0 < H) (hΔ : 0 < Δ)
    (g : I → J → V → ℝ)
    (hLip : ∀ i a, ∀ u v, |g i a u - g i a v| ≤ L*d u v)
    (hHeight : ∀ i a v, |g i a v| ≤ H)
    (hzero : ∀ i a, ∀ v ∈ interface R bag i, g i a v = 0)
    (i : I) (a : J) (ha : a ∈ A i) (u v : V) :
    2*|g (origin R A root i a) a u - g (origin R A root i a) a v| ≤
      ∑ t, |(state (ι := ι) R bag A g i).1 t u -
…

Mentions: OAI.BoundedTreewidthL1.RootedForest, OAI.BoundedTreewidthL1.TreeParticles.interface, OAI.BoundedTreewidthL1.TreeParticles.origin, OAI.BoundedTreewidthL1.TreeParticles.state

theorem OAI.BoundedTreewidthL1.TreeParticles.averaged_origin_realization line 131

Source documentation

Actual global averaged L1 realization of the branching preparation, with an unconditional integral lower bound from each deterministic active origin.

theorem averaged_origin_realization
    (G : SimpleGraph V) (hG : G.Connected) (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e)
    (T : SimpleGraph I) (hT : T.IsTree) (root : I) (B : I → Finset V)
    (hcover : ∀ v, ∃ i, v ∈ B i)
    (hedge : ∀ u v, G.Adj u v → ∃ i, u ∈ B i ∧ v ∈ B i)
    (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
    (A : I → Finset J) (k q : ℕ) (hbag : ∀ i, (B i).card ≤ k)
    (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q + k.factorial + 2)
    (ν : Measure Ω) [IsProbabilityMeasure ν]
    (L H Δ : ℝ) (hL : 0 < L) (hH : 0 < H) (hΔ : 0 < Δ)
    (g : Ω → I → J → V → ℝ) (hmeas : ∀ i a v, Measurable (fun ω => g ω i a v))
    (hLip : ∀ ω i a, ∀ u v, |g ω i a u - g ω i a v| ≤ L*shortestPathDistance G ℓ u v)
…

Mentions: OAI.BoundedTreewidthL1.shortestPathDistance

theorem OAI.BoundedTreewidthL1.LaunchNoise.uniform_coefficient_integral_lower line 211
def OAI.BoundedTreewidthL1.LaunchNoise.cobagBump line 249
def OAI.BoundedTreewidthL1.LaunchNoise.cobagNoise line 252
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagBump_eq_diff line 255
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagNoise_eq_diff line 280
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobag_diff_disjoint line 285
theorem OAI.BoundedTreewidthL1.LaunchNoise.cobag_partition_properties line 292
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagBump_bounds line 310
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagBump_zero line 315
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagBump_padding line 320
lemma OAI.BoundedTreewidthL1.LaunchNoise.coefficient_affine_integral_lower line 329
theorem OAI.BoundedTreewidthL1.LaunchNoise.cobag_partition_averaging line 357
def OAI.BoundedTreewidthL1.LaunchNoise.cobagLocationLaw line 386
def OAI.BoundedTreewidthL1.LaunchNoise.cobagLaw line 388
def OAI.BoundedTreewidthL1.LaunchNoise.cobagSample line 390
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagLocationLaw_probability line 395
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagLocationLaw_integral line 404
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagSample_continuous line 416
lemma OAI.BoundedTreewidthL1.LaunchNoise.cobagSample_integral line 427
theorem OAI.BoundedTreewidthL1.LaunchNoise.cobag_sampler line 441
abbrev OAI.BoundedTreewidthL1.LaunchNoise.FiniteSampleSpace line 509

theorem OAI.BoundedTreewidthL1.LaunchNoise.finite_padded_sampler line 514

Source documentation

Convert a finite padded partition law into the actual common sampler space, without selecting a partition or adding a separation assumption.

theorem finite_padded_sampler {V : Type*} [Fintype V] [MetricSpace V]
    (A : Set V) (μ : (V → V) → ℝ) (r α π : ℝ)
    (hμ : ∀ P, 0 ≤ μ P) (hμ₁ : ∑ P, μ P = 1)
    (hr : 0 < r) (hα : 0 < α) (hα1 : α ≤ 1)
    (hdiam : ∀ P, 0 < μ P → ∀ x y, P x = P y → dist x y ≤ r)
    (hpad : ∀ x, π ≤ ∑ P, if (∀ z, dist x z ≤ α*r → P z = P x) then μ P else 0) :
    ∃ ν : Measure (FiniteSampleSpace V), ∃ g : FiniteSampleSpace V → V → ℝ,
      IsProbabilityMeasure ν ∧ Measurable g ∧
      (∀ ω, LipschitzWith 1 (g ω) ∧ (∀ x, 0 ≤ g ω x ∧ g ω x ≤ r) ∧
        (∀ x ∈ A, g ω x = 0)) ∧
      ∀ x y, r < dist x y → (A.Nonempty → α*r ≤ infDist x A) →
        π*α*r/4 ≤ ∫ ω, |g ω x - g ω y| ∂ν := by
…

Mentions: OAI.BoundedTreewidthL1.LaunchNoise.FiniteSampleSpace

theorem OAI.BoundedTreewidthL1.LaunchNoise.graph_cobag_sampler line 565

Source documentation

The required uniformly padded co-bag launch now has an unconditional sampler in the original arbitrary-weight graph metric.

theorem graph_cobag_sampler :
    ∀ k : ℕ, 2 ≤ k → ∃ α π : ℝ, 0 < α ∧ α ≤ 1/8 ∧ 0 < π ∧ π ≤ 1 ∧
    ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V]
      (G : SimpleGraph V) (hG : G.Connected), HasTreeDecomposition G k →
      ∀ (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e),
      let : MetricSpace V := weightedMetricSpace G ℓ hG hℓ
…

Mentions: OAI.BoundedTreewidthL1.HasTreeDecomposition, OAI.BoundedTreewidthL1.weightedMetricSpace