AnalyticEndgame.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.Analytic.NoCornerInCoordinates line 10
Source documentation
No corner in every finite slope of the horizontal coordinate chart.
```
def NoCornerInCoordinates (μ : Plane → ℝ) : Prop :=
…
```
lemma OAI.GammaFPP.Analytic.norm_comp_swap line 14
lemma OAI.GammaFPP.Analytic.differentiable_horizontal_of_noCorner line 25
theorem OAI.GammaFPP.Analytic.differentiable_away_of_noCorner line 34
Source documentation
Absence of corners in both coordinate charts implies differentiability away from the origin for an arbitrary planar norm.
```
theorem differentiable_away_of_noCorner (μ : Plane → ℝ) (hμ : TimeConstantNorm μ)
    (hnc : NoCornerInCoordinates μ)
    (hncs : NoCornerInCoordinates (fun v => μ (swapPlane v))) :
    DifferentiableAwayFromOrigin μ := by
…
```
Mentions: OAI.GammaFPP.Analytic.NoCornerInCoordinates, OAI.GammaFPP.Analytic.swapPlane
lemma OAI.GammaFPP.Analytic.norm_profile_contDiff line 53
lemma OAI.GammaFPP.Analytic.differentiable_away_comp_swap line 76
theorem OAI.GammaFPP.Analytic.norm_sphere_curve_chart line 89
Source documentation
The unit sphere of a differentiable planar norm has regular C¹ curve charts with continuous local inverses.
```
theorem norm_sphere_curve_chart (μ : Plane → ℝ) (hμ : TimeConstantNorm μ)
    (hd : DifferentiableAwayFromOrigin μ) (v : Plane) (hv : μ v=1) :
    GammaFPP.HasC1CurveChart {z | μ z=1} v := by
…
```
Mentions: OAI.GammaFPP.HasC1CurveChart

theorem OAI.GammaFPP.Analytic.norm_boundary_curve_chart line 121

Source documentation

The topological frontier of the norm unit ball has regular C¹ curve charts.

theorem norm_boundary_curve_chart (μ : Plane → ℝ) (hμ : TimeConstantNorm μ)
    (hd : DifferentiableAwayFromOrigin μ) (v : Plane)
    (hv : v ∈ frontier {z | μ z ≤ 1}) :
    GammaFPP.HasC1CurveChart (frontier {z | μ z ≤ 1}) v := by
…

Mentions: OAI.GammaFPP.HasC1CurveChart

theorem OAI.GammaFPP.Analytic.analytic_endgame line 130

Source documentation

A planar norm with no corners in both coordinate charts is differentiable away from zero and has regular C¹ charts on its unit-ball frontier.

theorem analytic_endgame (μ : Plane → ℝ) (hμ : TimeConstantNorm μ)
    (hnc : NoCornerInCoordinates μ)
    (hncs : NoCornerInCoordinates (fun v => μ (swapPlane v))) :
    DifferentiableAwayFromOrigin μ ∧
      ∀ v ∈ frontier {z | μ z ≤ 1},
        GammaFPP.HasC1CurveChart (frontier {z | μ z ≤ 1}) v := by
…

Mentions: OAI.GammaFPP.Analytic.NoCornerInCoordinates, OAI.GammaFPP.Analytic.swapPlane, OAI.GammaFPP.HasC1CurveChart

theorem OAI.GammaFPP.Analytic.analytic_endgame_of_swap line 140

Source documentation

Symmetric norms need only the original horizontal no-corner statement.

theorem analytic_endgame_of_swap (μ : Plane → ℝ) (hμ : TimeConstantNorm μ)
    (hswap : ∀ v, μ (swapPlane v)=μ v) (hnc : NoCornerInCoordinates μ) :
    DifferentiableAwayFromOrigin μ ∧
      ∀ v ∈ frontier {z | μ z ≤ 1},
        GammaFPP.HasC1CurveChart (frontier {z | μ z ≤ 1}) v := by
…

Mentions: OAI.GammaFPP.Analytic.swapPlane, OAI.GammaFPP.Analytic.NoCornerInCoordinates, OAI.GammaFPP.HasC1CurveChart