FiniteStrips.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional algebra for the finite-strip construction. The image estimate and algebraic injectivity step do not require the analytic mass inequality.

def OAI.SymmetricMahler.measurement line 20
Source documentation
Apply the real matrix whose rows encode the strip constraints.
```
def measurement (A : J → I → ℝ) (v : I → ℝ) (j : J) : ℝ := ∑ i, A j i * v i
```
def OAI.SymmetricMahler.push line 23
Source documentation
Apply the transpose of the strip matrix to a vector of coefficients.
```
def push (A : J → I → ℝ) (p : J → ℝ) (i : I) : ℝ := ∑ j, A j i * p j
```
def OAI.SymmetricMahler.stripBody line 25
theorem OAI.SymmetricMahler.transpose_pairing line 29
Source documentation
The transpose identity in the image bound.
```
theorem transpose_pairing (A : J → I → ℝ) (p : J → ℝ) (v : I → ℝ) :
    (∑ i, push A p i * v i) = ∑ j, p j * measurement A v j := by
…
```
Mentions: OAI.SymmetricMahler.push, OAI.SymmetricMahler.measurement
theorem OAI.SymmetricMahler.image_bound line 40
Source documentation
Coefficients with bounded l1 norm define a bounded polar functional.
```
theorem image_bound (A : J → I → ℝ) (p : J → ℝ) (v : I → ℝ)
    (hv : v ∈ stripBody A) :
    (∑ i, push A p i * v i) ≤ ∑ j, |p j| := by
…
```
Mentions: OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.push
theorem OAI.SymmetricMahler.monotone_product_nonneg line 53
Source documentation
The scalar strict-monotonicity argument needs no derivative assumption.
```
theorem monotone_product_nonneg {f : ℝ → ℝ} (hf : StrictMono f) (a b : ℝ) :
    0 ≤ (f a - f b) * (a - b) := by
…
```
theorem OAI.SymmetricMahler.monotone_product_pos line 60

theorem OAI.SymmetricMahler.strict_pairing line 67

Source documentation

The positive sum in the injectivity argument.

theorem strict_pairing (A : J → I → ℝ)
    (hA : Function.Injective (measurement A))
    (f : J → ℝ → ℝ) (hf : ∀ j, StrictMono (f j))
    {y y' : I → ℝ} (hy : y ≠ y') :
    0 < ∑ j, (f j (measurement A y j) - f j (measurement A y' j)) *
      (measurement A y j - measurement A y' j) := by
…

Mentions: OAI.SymmetricMahler.measurement

theorem OAI.SymmetricMahler.vertical_map_injective line 83
Source documentation
Injectivity of the vertical map y ↦ Aᵀ (P_j ((Ay)_j)). This is the algebraic injectivity step for the finite-strip construction.
```
theorem vertical_map_injective (A : J → I → ℝ)
    (hA : Function.Injective (measurement A))
    (f : J → ℝ → ℝ) (hf : ∀ j, StrictMono (f j)) :
    Function.Injective (fun y : I → ℝ => push A (fun j => f j (measurement A y j))) := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.push

theorem OAI.SymmetricMahler.vertical_map_injOn line 119

Source documentation

The relevant vertical fibers need only support strict monotonicity on an interval, rather than on all of the real line.

theorem vertical_map_injOn (A : J → I → ℝ)
    (hA : Function.Injective (measurement A))
    (S : J → Set ℝ) (f : J → ℝ → ℝ)
    (hf : ∀ j, StrictMonoOn (f j) (S j)) :
    Set.InjOn (fun y : I → ℝ => push A (fun j => f j (measurement A y j)))
      {y | ∀ j, measurement A y j ∈ S j} := by
…

Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.push

theorem OAI.SymmetricMahler.full_map_injOn line 164

Source documentation

The full real map is injective when each vertical slice satisfies the hypotheses proved above. This also permits the fiber interval to depend on x.

theorem full_map_injOn (A : J → I → ℝ)
    (hA : Function.Injective (measurement A))
    (S : (I → ℝ) → J → Set ℝ) (f : (I → ℝ) → J → ℝ → ℝ)
    (hf : ∀ x j, StrictMonoOn (f x j) (S x j)) :
    Set.InjOn
      (fun z : (I → ℝ) × (I → ℝ) =>
        (z.1, push A (fun j => f z.1 j (measurement A z.2 j))))
      {z | ∀ j, measurement A z.2 j ∈ S z.1 j} := by
…

Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.push

theorem OAI.SymmetricMahler.coefficient_bound line 185

Source documentation

The planar uniform error accumulates only by the number of rows.

theorem coefficient_bound (p t : J → ℝ) (ε : ℝ)
    (hp : ∀ j, |p j| ≤ t j + ε) (ht : (∑ j, t j) < 1) :
    (∑ j, |p j|) < 1 + Fintype.card J * ε := by
…

theorem OAI.SymmetricMahler.image_bound_with_error line 194

Source documentation

The pointwise image estimate, including the planar error.

theorem image_bound_with_error (A : J → I → ℝ) (p t : J → ℝ) (ε : ℝ)
    (hp : ∀ j, |p j| ≤ t j + ε) (ht : (∑ j, t j) < 1)
    (v : I → ℝ) (hv : v ∈ stripBody A) :
    (∑ i, push A p i * v i) < 1 + Fintype.card J * ε :=
…

Mentions: OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.push