PrunedVariation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact variation cost of deleting original pairs

The full filtered measure is monotone in the coarse filter. Its pruned approximation differs by precisely the weighted mass of the removed pairs.

theorem OAI.Falconer.filteredPushforward_prune_variation line 17
theorem OAI.Falconer.finite_withDensity_of_bounded line 31
theorem OAI.Falconer.weighted_prune_variation_le line 40
theorem OAI.Falconer.withDensity_positive_of_lower line 56

theorem OAI.Falconer.filtered_masked_variation_le line 68

Source documentation

Smooth masks incur the same original-pair deletion cost as sharp pruning. The exceptional set is measured before the coarse filter is imposed.

theorem filtered_masked_variation_le (f : X → ℝ) (hf : Measurable f)
    (π : Measure X) (w m : X → ℝ≥0∞) [IsFiniteMeasure (π.withDensity w)]
    (hw : Measurable w) (hm : Measurable m) (hm1 : ∀ x, m x ≤ 1)
    (Γ B : Set X) (hΓ : MeasurableSet Γ) (C : ℝ≥0∞)
    (hbound : ∀ᵐ x ∂π, w x ≤ C) (hout : ∀ᵐ x ∂π, x ∉ B → m x = 1) :
    ∃ τ : FiniteMeasure ℝ,
      (τ : Measure ℝ) = ((π.restrict Γ).withDensity (fun x => w x*m x)).map f ∧
      PlanarFalconer.variationDistance
        ⟨filteredPushforward f (π.withDensity w) Γ,inferInstance⟩ τ ≤ C*π B := by
…

Mentions: OAI.PlanarFalconer.variationDistance, OAI.Falconer.filteredPushforward