PairPathMesh.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed meshes and height control of image paths

The mesh depends only on the requested error and the common path-length constant, not on the scale or on the endpoint. The actual L² height cocycle controls its finitely many samples; the common Lipschitz bounds then control every point of the image path.

theorem OAI.PolycyclicRecognition.exists_fixed_path_mesh line 23

Source documentation

A single finite mesh for the unit path interval.

theorem exists_fixed_path_mesh {δ : ℝ} (hδ : 0 < δ) :
    ∃ S : Finset (Set.Icc (0 : ℝ) 1),
      ∀ t, ∃ u ∈ S, dist t u ≤ δ := by
…

theorem OAI.PolycyclicRecognition.image_path_height_control line 41

Source documentation

Sampled height control extends to the whole image path, with the precise linear loss furnished by the Lipschitz constants and mesh spacing.

theorem image_path_height_control
    (p : NormalizedPair G Λ) (π : G →* Multiplicative W) (l : G →* Multiplicative W)
    {Lπ L r δ η ε : ℝ} (hLπ : 0 ≤ Lπ) (hL : 0 ≤ L) (hr : 0 ≤ r)
    (hπ : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ Lπ * dist x y)
    (γ : T → G) (hγ : ∀ t u, dist (γ t) (γ u) ≤ L * r * dist t u)
    (S : Finset T) (hmesh : ∀ t, ∃ u ∈ S, dist t u ≤ δ)
    (E : Set W)
    (hheight : ∀ u ∈ S, ∃ w ∈ E, ‖(l (γ u)).toAdd - r • w‖ ≤ ε * r)
    (herror : ∀ u ∈ S, ‖pairHeight π (γ u) p - (l (γ u)).toAdd‖ ≤ η * r) :
    ∀ t, ∃ w ∈ E,
      ‖pairHeight π (γ t) p - r • w‖ ≤ (Lπ * Λ * L * δ + η + ε) * r := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight

theorem OAI.PolycyclicRecognition.eLpNorm_pairHeight_error line 85
Source documentation
The norm in the actual Hilbert space equals the L² seminorm of the pointwise height error; there is no choice of pointwise representatives here.
```
theorem eLpNorm_pairHeight_error
    (π : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (l : G →* Multiplicative W) (g : G) :
    eLpNorm (fun p : NormalizedPair G Λ => pairHeight π g p - (l g).toAdd) 2 μ =
      ENNReal.ofReal ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.exists_pair_good_on_mesh line 98

Source documentation

The fixed finite-mesh selection for the actual normalized maps.

theorem exists_pair_good_on_mesh
    {I Y : Type*} [Fintype I] [MeasurableSpace Y]
    [MeasurableSpace G] [BorelSpace G] [MeasurableSpace W] [BorelSpace W]
    [SecondCountableTopology W]
    (ν : Measure Y) [IsProbabilityMeasure ν]
    (π : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (l : G →* Multiplicative W) (hl : Continuous fun g => (l g).toAdd)
    (γ : Y → I → G) (hγ : ∀ i, Measurable (fun y => γ y i))
    {a : ℝ} {η t : ℝ≥0∞} (hη : η ≠ 0) (hηtop : η ≠ ∞)
    (hbound : ∀ i y, ‖pairHeightL2 μ π hπ (γ y i) -
      Lp.const 2 μ (l (γ y i)).toAdd‖ ≤ a)
    (hsmall : (Fintype.card I : ℝ≥0∞) * (η⁻¹ ^ 2 * (ENNReal.ofReal a) ^ 2) < t) :
…

Mentions: OAI.PolycyclicRecognition.pairHeightL2