OAI/Analysis/LipschitzHilbert/Fourier/WitnessProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Horizontal projection size of actual compact popularity witnesses.

  1. theorem OAI.LipschitzHilbert.projection_measure_bound line 18

    Source documentation

    A compact set confined between two parallel lines has area at most its horizontal projection length times its vertical thickness.

    theorem projection_measure_bound (E : Set (ℝ × ℝ)) (hE : IsCompact E)
    {s c B : ℝ} (hB : 0 ≤ B)
    (hstrip : ∀ z ∈ E, |z.2 - s * z.1 - c| ≤ B) :
    (volume.prod volume).real E ≤ 2 * B * volume.real (Prod.fst '' E) := by
…
  2. theorem OAI.LipschitzHilbert.SlopeBox.witness_projection_lower line 53

    Source documentation

    The compact witness occupies a substantial horizontal set solely from its area and the box-width bound. No measurable selection of fibers is used.

    theorem witness_projection_lower (T : SlopeBox) (E : Set (ℝ × ℝ)) (hE : IsCompact E)
    {A q : ℝ} (hA : 0 < A) (hbox : ∀ z ∈ E, T.radius z ≤ A)
    (harea : q * T.length * T.width ≤ (volume.prod volume).real E) :
    q * T.length / (2 * A) ≤ volume.real (Prod.fst '' E) := by
…

    Mentions: OAI.LipschitzHilbert.SlopeBox