PublishedInputs.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Published inputs for the Lipschitz-direction Hilbert transform

The two classical estimates used by the manuscript are stated as propositions. Their deterministic consequences make the quantifiers needed for the finite rectangle and martingale applications explicit.

Lacey--Li, On a conjecture of E. M. Stein on the Hilbert transform on vector fields, Memoirs AMS 205 (2010), no. 965, result 1.10 and equation (1.11); DOI 10.1090/S0065-9266-10-00572-7. In the author version arXiv:0704.0808 these occur on printed p. 3, with the finite-family proof in Chapter 3. This is the published form of arXiv:math/0601213v2, Theorem 1.4. We use the finite admissible-rectangle weak (2,2) estimate.
Zorin-Kranich, Weighted Lépingle inequality, Bernoulli 26 (2020), 2311--2318, Theorem 1.1, with p = 2, r = 3, and weight one. We use only real-valued finite martingales on probability spaces.

The deterministic consequences below make the quantifiers relevant to the application explicit: a union of high-average rectangles, and a variation sum whose increasing indices may be chosen separately at each point.

abbrev OAI.LipschitzHilbert.Plane line 38
Also declared: ComparatorChallenges/LipschitzHilbert.lean:15 (same declaration text).
structure OAI.LipschitzHilbert.Rectangle line 41
Source documentation
A closed orthogonal rectangle; long and short are full side lengths.
```
structure Rectangle where
…
```
def OAI.LipschitzHilbert.Rectangle.carrier line 51
theorem OAI.LipschitzHilbert.Rectangle.measurableSet_carrier line 55
def OAI.LipschitzHilbert.Rectangle.popularSet line 63
Source documentation
The arc of total angular length short / long about the long-side direction. The field is separately required to have unit norm.
```
def popularSet (R : Rectangle) (v : Plane → Plane) : Set Plane :=
…
```
Mentions: OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.Plane
def OAI.LipschitzHilbert.Rectangle.Admissible line 67
Source documentation
Admissibility uses the long-side length restriction, with no restriction when K = 0.
```
def Admissible (R : Rectangle) (v : Plane → Plane) (K δ : ℝ≥0) : Prop :=
…
```
Mentions: OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.Plane
def OAI.LipschitzHilbert.Rectangle.average line 71
def OAI.LipschitzHilbert.rectangleMaximum line 77
Source documentation
The finite-rectangle maximal function appearing in the needed specialization.
```
def rectangleMaximum {ι : Type*} [Fintype ι] (R : ι → Rectangle)
    (h : Plane → ℝ) (x : Plane) : ℝ≥0∞ :=
…
```
Mentions: OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.Plane
def OAI.LipschitzHilbert.squareIntegral line 84
Source documentation
Squared L² size; using the nonnegative integral also covers intermediate expressions.
```
def squareIntegral {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (h : Ω → ℝ) : ℝ≥0∞ := ∫⁻ x, ‖h x‖ₑ ^ 2 ∂μ
```
def OAI.LipschitzHilbert.LaceyLiInput line 90
Source documentation
Lacey--Li, published result 1.10 / equation (1.11), specialized to finite families in squared weak-type form (also arXiv:math/0601213v2, Theorem 1.4). C is the weak L² operator constant before squaring.
```
def LaceyLiInput : Prop :=
…
```
theorem OAI.LipschitzHilbert.rectangle_union_subset_level line 101
Source documentation
If every selected rectangle has a high average, their union lies in the level set.
```
theorem rectangle_union_subset_level {ι : Type*} [Fintype ι]
    (R : ι → Rectangle) (h : Plane → ℝ) (t : ℝ≥0)
    (havg : ∀ i, (t : ℝ≥0∞) < (R i).average h) :
    (⋃ i, (R i).carrier) ⊆ {x | (t : ℝ≥0∞) < rectangleMaximum R h x} := by
…
```
Mentions: OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.Plane, OAI.LipschitzHilbert.rectangleMaximum

theorem OAI.LipschitzHilbert.disjoint_witness_packing line 117

Source documentation

Disjoint popularity witnesses turn a covering bound into a weighted packing bound. In the manuscript, w i is a top rectangle's area and a its popularity lower bound.

theorem disjoint_witness_packing {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι]
    (μ : Measure Ω) (E R : ι → Set Ω) (w : ι → ℝ≥0∞) (a : ℝ≥0∞)
    (hmeas : ∀ i, MeasurableSet (E i))
    (hdisj : Pairwise fun i j => Disjoint (E i) (E j))
    (hsub : ∀ i, E i ⊆ R i) (hsize : ∀ i, a * w i ≤ μ (E i)) :
    a * ∑ i, w i ≤ μ (⋃ i, R i) := by
…

theorem OAI.LipschitzHilbert.laceyLi_union_bound line 131

Source documentation

The precise covering consequence used for the popular-top count.

theorem laceyLi_union_bound (hLL : LaceyLiInput) :
    ∃ C : ℝ≥0, 0 < C ∧
      ∀ (v : Plane → Plane) (K δ : ℝ≥0),
        LipschitzWith K v → (∀ x, ‖v x‖ = 1) → 0 < δ → δ < 1 →
        ∀ (n : ℕ) (R : Fin n → Rectangle),
          (∀ i, (R i).Admissible v K δ) →
          ∀ (h : Plane → ℝ), MemLp h 2 volume → ∀ t : ℝ≥0, 0 < t →
            (∀ i, (t : ℝ≥0∞) < (R i).average h) →
            (t : ℝ≥0∞) ^ 2 * volume (⋃ i, (R i).carrier) ≤
              (C : ℝ≥0∞) ^ 2 / (δ : ℝ≥0∞) * squareIntegral volume h := by
…

Mentions: OAI.LipschitzHilbert.LaceyLiInput, OAI.LipschitzHilbert.Plane, OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.squareIntegral

def OAI.LipschitzHilbert.variationCube line 149
Source documentation
Cubed variation of a finite scalar sequence. Repetitions in the monotone list allow every shorter partition to be padded to length N + 1.
```
def variationCube {Ω : Type*} (F : ℕ → Ω → ℝ) (N : ℕ) (x : Ω) : ℝ≥0∞ :=
…
```
def OAI.LipschitzHilbert.LepingleInput line 159
Source documentation
Lépingle's unweighted scalar L² bound for 3-variation. The constant is uniform in the probability space, the filtration, and the finite horizon.
```
def LepingleInput : Prop :=
…
```

theorem OAI.LipschitzHilbert.selected_variation_le line 169

Source documentation

Pointwise-selected increasing partitions are controlled by the full variation.

theorem selected_variation_le {Ω : Type*} (F : ℕ → Ω → ℝ) (N : ℕ)
    (p : Ω → Fin (N + 1) → Fin (N + 1)) (hp : ∀ x, Monotone (p x)) (x : Ω) :
    (∑ i : Fin N, ‖F (p x i.succ) x - F (p x i.castSucc) x‖ₑ ^ 3) ≤
      variationCube F N x := by
…

Mentions: OAI.LipschitzHilbert.variationCube

theorem OAI.LipschitzHilbert.lepingle_selected_bound line 182

Source documentation

The published estimate also permits the endpoints to depend on the point. No measurability of the selection is needed for the nonnegative upper integral.

theorem lepingle_selected_bound (hL : LepingleInput) :
    ∃ C : ℝ≥0, 0 < C ∧
      ∀ (Ω : Type) (m : MeasurableSpace Ω) (μ : Measure Ω),
        IsProbabilityMeasure μ →
        ∀ (ℱ : Filtration ℕ m) (F : ℕ → Ω → ℝ),
          Martingale F ℱ μ → (∀ n, MemLp (F n) 2 μ) → ∀ (N : ℕ)
            (p : Ω → Fin (N + 1) → Fin (N + 1)),
            (∀ x, Monotone (p x)) →
            (∫⁻ x, (∑ i : Fin N,
              ‖F (p x i.succ) x - F (p x i.castSucc) x‖ₑ ^ 3) ^ (2 / 3 : ℝ) ∂μ) ≤
              (C : ℝ≥0∞) ^ 2 * squareIntegral μ (F N) := by
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.squareIntegral