DescriptorEnvelope.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual descriptor tests used by the angular envelope

These are finite intersections of the original endpoint tests. Passing to retained lists only weakens these support conditions. No deletion of an angular factor or analytic estimate is inferred from this set inclusion.

def OAI.Falconer.descriptorListGood line 20
theorem OAI.Falconer.descriptorListGood_measurable line 25
theorem OAI.Falconer.descriptorListGood_antitone line 35
theorem OAI.Falconer.policy_descriptorListGood_mono line 41
theorem OAI.Falconer.remaining_descriptorListGood_mono line 48
theorem OAI.Falconer.minimal_policy_descriptorListGood line 56

theorem OAI.Falconer.descriptorListGood_parallel_test line 66

Source documentation

This uses the continuous profile at the actual normalized integer depths.

theorem descriptorListGood_parallel_test (Q : DyadicCube d) (hQ : Q.side = 1)
    (ρ : Measure (Space d)) (m : ℝ → ℝ) (N : ℕ) (σ : ℝ) (J i : ℕ)
    (B : Finset PolicyDescriptor) {a g p : ℕ} (hag : a ≤ g) (hgp : g ≤ p)
    (hB : PolicyDescriptor.parallel g p ∈ B)
    (X P : List (Fin d → Bool)) (hX : X.length = a) (hP : P.length = p-a)
    {x : Space d} (hx : x ∈ ((Q.descendant X).descendant P).carrier)
    (w : Sphere d)
    (hw : (x,w) ∈ descriptorListGood Q ρ (fun t => m (t/N)) N σ J i B) :
    DyadicParallelTest (Q.descendant X) ((Q.descendant X).occupiedPaths ρ (p-a))
      (g-a) P w (angularTestWidth N σ J i p)
      ⌈((2:ℝ)^N)^(PlanarFalconer.height
        (fun j : ℕ => m ((j:ℝ)/N)-((d:ℝ)/2)*(j:ℝ)/N) g p+
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.descriptorListGood, OAI.Falconer.DyadicParallelTest, OAI.Falconer.angularTestWidth, OAI.PlanarFalconer.height

theorem OAI.Falconer.originDescriptors_subset_policy line 83

Source documentation

The origin chosen by the scalar policy is among its actual descriptor list.

theorem originDescriptors_subset_policy (A : ℕ → ℝ) {N q a t : ℕ}
    (ht : t ≤ N) (hwide : a+100*q < t) :
    PlanarFalconer.originDescriptors A N q a t ⊆ policyDescriptorList A N q a t := by
…

Mentions: OAI.PlanarFalconer.originDescriptors

theorem OAI.Falconer.originDescriptors_subset_remaining line 93
theorem OAI.Falconer.origin_parallel_mem_remaining line 101

theorem OAI.Falconer.AngularAdmissible.descriptorList_subset line 114

Source documentation

List support may be weakened while preserving the same analytic symbol budget.

theorem AngularAdmissible.descriptorList_subset {n k : ℕ} {D : ℝ}
    (Q : DyadicCube (n+2)) (ρ : Measure (Space (n+2)))
    (m : ℝ → ℝ) (N : ℕ) (σ : ℝ) (J i : ℕ)
    {B C : Finset PolicyDescriptor} (hCB : C ⊆ B)
    {b : Space (n+2) → Sphere (n+2) → ℂ}
    (hb : AngularAdmissible k D (descriptorListGood Q ρ m N σ J i B) b) :
    AngularAdmissible k D (descriptorListGood Q ρ m N σ J i C) b :=
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.AngularAdmissible, OAI.Falconer.descriptorListGood