OAI/MeasureTheory/Falconer/Shells/PositiveSuffix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Falconer.suffix_policy_projection_mem line 14
2. theorem OAI.Falconer.policy_descriptor_end_bounds line 27
3. def OAI.Falconer.policyTestPairs line 33
4. theorem OAI.Falconer.uniform_policy_suffix_collision line 40

   Source documentation

   The suffix collision estimate uses the actual tested pair measures, with a coarser policy list at the next smoothing index.

   theorem uniform_policy_suffix_collision {σ : ℝ} (hσ : 0 < σ)
       {J : ℕ} (hJ : 0 < J) :
       ∃ N₀ : ℕ, ∀ N ≥ N₀, ∀ (Q : DyadicCube d), Q.side = 1 →
         ∀ (ρ : Measure (Space d)) [IsFiniteMeasure ρ] (m : ℝ → ℝ) (A : ℕ → ℝ)
           (q a p t i : ℕ), 0 < q → t ≤ N → a+100*q < t →
           p = PlanarFalconer.policyDepth A N q a t → a+t < 2*p → i ≤ J →
         ∀ (w₀ : Sphere d) (X Y : List (Fin d → Bool)), X.length = a → Y.length = a →
         125*((d:ℝ)+1)*(Q.descendant X).side ≤
           ‖(Q.descendant X).center-(Q.descendant Y).center‖ →
         ((testedCellDistance ρ ρ (Q.descendant X) (Q.descendant Y)
             (policyTestPairs w₀ Q ρ m A N σ J i q a t)).prod
           (testedCellDistance ρ ρ (Q.descendant X) (Q.descendant Y)
   …

   Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.PlanarFalconer.policyDepth, OAI.Falconer.Sphere, OAI.Falconer.testedCellDistance, OAI.Falconer.policyTestPairs

5. def OAI.Falconer.positiveCollisionCount line 150
6. theorem OAI.Falconer.positiveCollisionCount_ne_top line 160
7. theorem OAI.Falconer.positive_suffix_prefactor line 167
8. theorem OAI.Falconer.uniform_policy_suffix_count line 182