LaunchNoise.lean`

77 declarations, 0 contain sorry, 0 declared as axioms

Two deterministic shifted dyadic grids. A fair choice has the same one-half interior probability needed by ordinary launch noise.

def OAI.BoundedTreewidthL1.LaunchNoise.bump line 11
def OAI.BoundedTreewidthL1.LaunchNoise.noise line 15
lemma OAI.BoundedTreewidthL1.LaunchNoise.bump_lipschitz line 18
lemma OAI.BoundedTreewidthL1.LaunchNoise.bump_bounds line 27
lemma OAI.BoundedTreewidthL1.LaunchNoise.bump_zero line 35
lemma OAI.BoundedTreewidthL1.LaunchNoise.bump_le_dist line 40
lemma OAI.BoundedTreewidthL1.LaunchNoise.bump_padding line 46
theorem OAI.BoundedTreewidthL1.LaunchNoise.bump_properties line 57
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_at line 66
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_zero line 78
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_nonneg line 82
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_upper line 87
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_one_sided line 95
theorem OAI.BoundedTreewidthL1.LaunchNoise.disjoint_noise line 120
def OAI.BoundedTreewidthL1.LaunchNoise.bandIndex line 142
def OAI.BoundedTreewidthL1.LaunchNoise.bandLower line 143
def OAI.BoundedTreewidthL1.LaunchNoise.gridFactor line 145
lemma OAI.BoundedTreewidthL1.LaunchNoise.band_bounds line 147
lemma OAI.BoundedTreewidthL1.LaunchNoise.bandIndex_eq line 161
lemma OAI.BoundedTreewidthL1.LaunchNoise.band_same line 174
lemma OAI.BoundedTreewidthL1.LaunchNoise.gridFactor_pos line 179
theorem OAI.BoundedTreewidthL1.LaunchNoise.two_grid_margin line 182
Source documentation
Every positive height lies well inside one of the two grids.
```
theorem two_grid_margin (t : ℝ) (ht : 0 < t) :
    ∃ b : Bool, t/8 ≤ t - bandLower (gridFactor b) t ∧
      t/8 ≤ 2 * bandLower (gridFactor b) t - t := by
…
```
Mentions: OAI.BoundedTreewidthL1.LaunchNoise.bandLower, OAI.BoundedTreewidthL1.LaunchNoise.gridFactor
def OAI.BoundedTreewidthL1.FiniteProductLaw.mass line 213
lemma OAI.BoundedTreewidthL1.FiniteProductLaw.nonneg line 214
lemma OAI.BoundedTreewidthL1.FiniteProductLaw.total line 218
lemma OAI.BoundedTreewidthL1.FiniteProductLaw.factor_pos line 224
lemma OAI.BoundedTreewidthL1.FiniteProductLaw.event line 232
def OAI.BoundedTreewidthL1.LaunchNoise.MetricPaddedSupply line 263
def OAI.BoundedTreewidthL1.LaunchNoise.GoodBump line 270
def OAI.BoundedTreewidthL1.LaunchNoise.HasOrdinaryBumps line 275
def OAI.BoundedTreewidthL1.LaunchNoise.bandSet line 288
def OAI.BoundedTreewidthL1.LaunchNoise.bandKey line 291
def OAI.BoundedTreewidthL1.LaunchNoise.bandScale line 294
def OAI.BoundedTreewidthL1.LaunchNoise.locationSet line 297
lemma OAI.BoundedTreewidthL1.LaunchNoise.locationSet_disjoint line 301
lemma OAI.BoundedTreewidthL1.LaunchNoise.location_self line 312
lemma OAI.BoundedTreewidthL1.LaunchNoise.bandScale_pos line 318
lemma OAI.BoundedTreewidthL1.LaunchNoise.bandScale_at line 324
lemma OAI.BoundedTreewidthL1.LaunchNoise.bump_noise_bounds line 329
lemma OAI.BoundedTreewidthL1.LaunchNoise.location_ball line 350
lemma OAI.BoundedTreewidthL1.LaunchNoise.good_location line 378
lemma OAI.BoundedTreewidthL1.LaunchNoise.ordinary_bumps_reindex line 416
def OAI.BoundedTreewidthL1.LaunchNoise.locationMass line 455
lemma OAI.BoundedTreewidthL1.LaunchNoise.locationMass_nonneg line 460
lemma OAI.BoundedTreewidthL1.LaunchNoise.locationMass_total line 468
lemma OAI.BoundedTreewidthL1.LaunchNoise.locationMass_event line 478
theorem OAI.BoundedTreewidthL1.LaunchNoise.finite_ordinary_bumps line 507
Source documentation
Finite ordinary noise from a padded supply, which is available unconditionally for the weighted graph metrics by PaddedConstruction.
```
theorem finite_ordinary_bumps
    (h : V → ℝ) (hh : LipschitzWith 1 h) (h0 : ∀ x, 0 ≤ h x)
    (α π η : ℝ) (hα : 0 < α) (hα8 : α ≤ 1/8) (hη : 0 < η) (hη4 : η < 1/4)
    (hsupply : MetricPaddedSupply (V := V) α π) : HasOrdinaryBumps h α π η := by
…
```
Mentions: OAI.BoundedTreewidthL1.LaunchNoise.MetricPaddedSupply, OAI.BoundedTreewidthL1.LaunchNoise.HasOrdinaryBumps
def OAI.BoundedTreewidthL1.LaunchNoise.locationLaw line 579
abbrev OAI.BoundedTreewidthL1.LaunchNoise.CoeffCube line 581
abbrev OAI.BoundedTreewidthL1.LaunchNoise.NoiseSpace line 582
def OAI.BoundedTreewidthL1.LaunchNoise.noiseLaw line 583
def OAI.BoundedTreewidthL1.LaunchNoise.noiseXi line 585
def OAI.BoundedTreewidthL1.LaunchNoise.noiseV line 586
def OAI.BoundedTreewidthL1.LaunchNoise.noiseG line 588
lemma OAI.BoundedTreewidthL1.LaunchNoise.locationLaw_apply line 592
lemma OAI.BoundedTreewidthL1.LaunchNoise.locationLaw_probability line 597
lemma OAI.BoundedTreewidthL1.LaunchNoise.noiseLaw_probability line 604
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_locationLaw line 610
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_goodProbability line 617
lemma OAI.BoundedTreewidthL1.LaunchNoise.noiseXi_measurable line 631
lemma OAI.BoundedTreewidthL1.LaunchNoise.noiseV_measurable line 635
lemma OAI.BoundedTreewidthL1.LaunchNoise.noiseG_measurable line 648
lemma OAI.BoundedTreewidthL1.LaunchNoise.noiseXi_uniform line 654
lemma OAI.BoundedTreewidthL1.LaunchNoise.noiseXi_indep line 664
lemma OAI.BoundedTreewidthL1.LaunchNoise.cube_uniform line 681
lemma OAI.BoundedTreewidthL1.LaunchNoise.cube_independent line 686

lemma OAI.BoundedTreewidthL1.LaunchNoise.fresh_noise line 691

Source documentation

Fresh independent randomness works with any previously constructed probability space.

lemma fresh_noise {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν]
    {V : Type*} {n m : ℕ} (μ : Fin n → ℝ)
    (hμ : ∀ a, 0 ≤ μ a) (hμ₁ : ∑ a, μ a = 1)
    (h : V → ℝ) (φ : Fin n → Fin m → V → ℝ) :
    IndepFun (fun ω : Ω × NoiseSpace n m => ω.1)
      (fun ω => noiseG h φ ω.2) (ν.prod (noiseLaw m μ)) := by
…

Mentions: OAI.BoundedTreewidthL1.LaunchNoise.NoiseSpace, OAI.BoundedTreewidthL1.LaunchNoise.noiseG, OAI.BoundedTreewidthL1.LaunchNoise.noiseLaw

lemma OAI.BoundedTreewidthL1.LaunchNoise.noiseXi_uniform_interval line 700
lemma OAI.BoundedTreewidthL1.LaunchNoise.noise_deterministic line 713
def OAI.BoundedTreewidthL1.LaunchNoise.HasOrdinaryNoise line 766
Source documentation
Complete finite ordinary-noise sampler; its law is the displayed product of a fresh uniform xi, a finite location law, and independent uniform amplitudes.
```
def HasOrdinaryNoise {V : Type*} [MetricSpace V]
    (h : V → ℝ) (α π η : ℝ) : Prop :=
…
```
theorem OAI.BoundedTreewidthL1.LaunchNoise.metric_ordinary_noise line 794

theorem OAI.BoundedTreewidthL1.LaunchNoise.graph_ordinary_noise line 814

Source documentation

Uniform graph-metric input; the distance is definitionally the original positive-weight shortest-path distance, with no edge-ratio restriction.

theorem graph_ordinary_noise (k : ℕ) (hk : 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 := weightedMetricSpace G ℓ hG hℓ
…

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

lemma OAI.BoundedTreewidthL1.TreeCache.fresh_eq_singleton line 851
lemma OAI.BoundedTreewidthL1.TreeCache.origin_self line 872
lemma OAI.BoundedTreewidthL1.bagDistance_eq_infDist line 888
structure OAI.BoundedTreewidthL1.LaunchNoise.OrdinarySeed line 908
Source documentation
The complete finite launch data, retaining both independent uniform variables and the random good-bump event required in the non-collapse argument.
```
structure OrdinarySeed {V : Type*} [MetricSpace V] (h : V → ℝ) (α π η : ℝ) where
…
```
lemma OAI.BoundedTreewidthL1.LaunchNoise.OrdinarySeed.exists_of_has line 932