DescriptorRemoval.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Removing exactly the reached descriptor factors from positive energy

theorem OAI.Falconer.descriptorProduct_mul_norm_le line 13

theorem OAI.Falconer.independentAngularEnergy_descriptorProduct_remove line 27

Source documentation

The spatially constant factors are removed only after squaring and integrating. Every descriptor with an anchor deeper than the child remains.

theorem independentAngularEnergy_descriptorProduct_remove
    (Q : DyadicCube d) (hQ : 0 < Q.side) (ρ : Measure (Space d))
    (m : ℝ → ℝ) (N : ℕ) (σ : ℝ) (J i : ℕ) (B : Finset PolicyDescriptor)
    (S : PolicyDescriptor → Finset (Sphere d))
    (hcover : ∀ c ∈ B, ∀ w : Sphere d,
      ∃ z ∈ S c, dist w z ≤ descriptorMaskRadius N σ c/2)
    (X Y : List (Fin d → Bool)) (μ ν : Measure (Space d))
    [IsFiniteMeasure μ] [IsFiniteMeasure ν] {M₁ M₂ : ℝ}
    (hM₁ : 0 < M₁) (hM₂ : 0 < M₂)
    (b c : Space d → Sphere d → ℂ)
    (hb : Measurable (Function.uncurry b)) (hc : Measurable (Function.uncurry c))
    {C₁ C₂ : ℝ} (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂)
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.descriptorMaskRadius