OAI/MeasureTheory/Falconer/Estimates/WeightedLowpass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Falconer.restrict_smul_le_withDensity line 20

   Source documentation

   A lower bound only on the tested set suffices for positive domination.

   theorem restrict_smul_le_withDensity {X : Type*} [MeasurableSpace X]
       (μ : Measure X) (G : Set X) (hG : MeasurableSet G)
       (w : X → ℝ≥0∞) (c : ℝ≥0∞)
       (h : ∀ᵐ x ∂μ, x ∈ G → c ≤ w x) :
       c • μ.restrict G ≤ μ.withDensity w := by
   …

2. theorem OAI.Falconer.dyadic_collision_fourier_of_domination line 33
3. def OAI.Falconer.descriptorPairWeight line 54
4. theorem OAI.Falconer.descriptorPairWeight_measurable line 63
5. def OAI.Falconer.maskedCellDistance line 73
6. theorem OAI.Falconer.maskedCellDistance_dominates line 84

   Source documentation

   Core masks preserve the original tested pairs; only their distance weight enters the domination constant.

   theorem maskedCellDistance_dominates
       (w₀ : Sphere d) (Q : DyadicCube d) (ρ : Measure (Space d))
       (m : ℝ → ℝ) (N : ℕ) (σ : ℝ) (J i a : ℕ)
       (B : Finset PlanarFalconer.PolicyDescriptor)
       (S : PlanarFalconer.PolicyDescriptor → Finset (Sphere d))
       (X Y : DyadicCube d) (G : Set (Space d × Space d)) (hG : MeasurableSet G)
       (c : ℝ) (_hc : 0 ≤ c)
       (hcore : ∀ᵐ z ∂(ρ.restrict X.carrier).prod (ρ.restrict Y.carrier), z ∈ G →
         descriptorProduct Q ρ (fun u => m (u/N)) N σ J i B S z.1 (normalizeToSphere w₀ (z.1-z.2)) = 1 ∧
         descriptorProduct Q ρ (fun u => m (u/N)) N σ J i B S z.2 (normalizeToSphere w₀ (z.1-z.2)) = 1)
       (hweight : ∀ᵐ z ∂(ρ.restrict X.carrier).prod (ρ.restrict Y.carrier), z ∈ G →
         c ≤ (dist z.1 z.2*(2:ℝ)^a)^(-(((d:ℝ)-1)/2))) :
   …

   Mentions: OAI.Falconer.Sphere, OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.PlanarFalconer.PolicyDescriptor, OAI.Falconer.descriptorProduct, OAI.Falconer.normalizeToSphere

7. theorem OAI.Falconer.profileModelMass_inverse_four line 112
8. theorem OAI.Falconer.masked_distance_collision_lowpass line 120