ClockPolar.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Continuous polar correction of the actual clock path

The correction is the fixed formula x (x* x)^(-1/2). Both Gram bounds come from the proved three-term cancellation estimates. Continuity and exact endpoint preservation are proved for this formula; no cocycle or half-flip equation is assumed or concluded.

def OAI.WeakPureInfiniteness.clockPolarValue line 25
Source documentation
The explicit polar correction, on the open set used below.
```
def clockPolarValue (x : E) : E := x * CFC.rpow (star x * x) (-1 / 2 : ℝ)
```
lemma OAI.WeakPureInfiniteness.clockPolarValue_mem line 27
lemma OAI.WeakPureInfiniteness.clockPolarValue_of_unitary line 34

lemma OAI.WeakPureInfiniteness.clockPolarValue_continuous line 39

Source documentation

Continuity uses strict positivity of the actual initial Gram element.

lemma clockPolarValue_continuous {X : Type*} [TopologicalSpace X] (f : X → E)
    (hf : Continuous f) (hi : ∀ t, IsUnit (star (f t) * f t)) :
    Continuous (fun t => clockPolarValue (f t)) := by
…

Mentions: OAI.WeakPureInfiniteness.clockPolarValue

lemma OAI.WeakPureInfiniteness.exists_clockPolar_tolerance line 51

Source documentation

A uniform tolerance for this explicit correction, not an unspecified choice of a nearby unitary.

lemma exists_clockPolar_tolerance [Nontrivial E] (ε : ℝ) (hε : 0 < ε) :
    ∃ τ : ℝ, 0 < τ ∧ τ ≤ 1 ∧ ∀ x : E,
      ‖star x * x - 1‖ < τ → ‖x * star x - 1‖ < τ →
      clockPolarValue x ∈ unitary E ∧ ‖clockPolarValue x - x‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.clockPolarValue

lemma OAI.WeakPureInfiniteness.exists_clockCorrected_unitary_path line 91

Source documentation

The actual clock-corrected cancellation has a continuous unitary polar correction, with both original endpoints unchanged and uniform error.

lemma exists_clockCorrected_unitary_path [Nontrivial E] (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (k : unitary E) (a b u : E),
      star a * a = 1 → star b * b = 1 → star a * b = 0 → u ∈ unitary E →
      ‖a * (k : E) - (k : E) * a‖ ≤ δ →
      ‖b * (k : E) - (k : E) * b‖ ≤ δ →
      ‖u * (k : E) - (k : E) * u‖ ≤ δ →
      ∃ p : ℝ → unitary E, Continuous p ∧
        (p 0 : E) = cornerCompression a u * cornerCompression b (star u) ∧
        (p (Real.pi / 2) : E) = 1 ∧
        (∀ θ, Joined (1 : unitary E) (p θ)) ∧
        ∀ θ, ‖(p θ : E) - clockCorrectedCancellation k a b u θ‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.cornerCompression, OAI.WeakPureInfiniteness.clockCorrectedCancellation

lemma OAI.WeakPureInfiniteness.clockPolar_isometry_norm line 142
lemma OAI.WeakPureInfiniteness.clockPolar_corner_norm line 147

lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_sub_norm_le line 158

Source documentation

The explicit corrected polynomial retains a uniform angular bound, independently of the clock and of the constituent unitary.

lemma clockCorrectedCancellation_sub_norm_le (k : unitary E) (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hu : u ∈ unitary E)
    (θ φ : ℝ) :
    ‖clockCorrectedCancellation k a b u θ - clockCorrectedCancellation k a b u φ‖ ≤
      16 * |θ - φ| := by
…

Mentions: OAI.WeakPureInfiniteness.clockCorrectedCancellation

lemma OAI.WeakPureInfiniteness.clockCorrected_near_path_sample_bound line 222

Source documentation

Uniform closeness suffices for sampling the polar path; no Lipschitz property of the functional-calculus correction is assumed.

lemma clockCorrected_near_path_sample_bound (k : unitary E) (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hu : u ∈ unitary E)
    (p : ℝ → unitary E) (η : ℝ)
    (hp : ∀ θ, ‖(p θ : E) - clockCorrectedCancellation k a b u θ‖ ≤ η)
    (θ φ : ℝ) : ‖(p θ : E) - p φ‖ ≤ 16 * |θ - φ| + 2 * η := by
…

Mentions: OAI.WeakPureInfiniteness.clockCorrectedCancellation