AnalyticSpecialization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.Analytic.NoCornerWedge line 10
Source documentation
The slope wedge used by the manuscript's probabilistic argument.
```
def NoCornerWedge (μ : Plane → ℝ) : Prop :=
…
```
theorem OAI.GammaFPP.Analytic.differentiable_away_of_noCornerWedge line 17
Source documentation
Coordinate-swap symmetry and norm homogeneity extend absence of corners on the slope wedge to differentiability at every nonzero vector.
```
theorem differentiable_away_of_noCornerWedge (μ : Plane → ℝ)
    (hμ : TimeConstantNorm μ) (hswap : ∀ v, μ (swapPlane v)=μ v)
    (hnc : NoCornerWedge μ) : DifferentiableAwayFromOrigin μ := by
…
```
Mentions: OAI.GammaFPP.Analytic.swapPlane, OAI.GammaFPP.Analytic.NoCornerWedge

theorem OAI.GammaFPP.Analytic.gammaMeanNorm_analytic_of_noCorner line 54

Source documentation

Absence of corners on the slope wedge gives differentiability and regular boundary charts for the Gamma mean norm.

theorem gammaMeanNorm_analytic_of_noCorner
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (hnc : NoCornerWedge (gammaMeanNorm h hs hr)) :
    DifferentiableAwayFromOrigin (gammaMeanNorm h hs hr) ∧
      ∀ v ∈ frontier {z | gammaMeanNorm h hs hr z ≤ 1},
        GammaFPP.HasC1CurveChart (frontier {z | gammaMeanNorm h hs hr z ≤ 1}) v := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.Analytic.NoCornerWedge, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.HasC1CurveChart

theorem OAI.GammaFPP.Analytic.gammaMeanNorm_target_conjunction_of_inputs line 66

Source documentation

A time-constant property and absence of corners on the slope wedge identify the Gamma mean norm as a differentiable limit norm with regular boundary charts.

theorem gammaMeanNorm_target_conjunction_of_inputs
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (ht : IsTimeConstant P τ (gammaMeanNorm h hs hr))
    (hnc : NoCornerWedge (gammaMeanNorm h hs hr)) :
    ∃ μ : Plane → ℝ, TimeConstantNorm μ ∧ IsTimeConstant P τ μ ∧
      DifferentiableAwayFromOrigin μ ∧
      ∀ v ∈ frontier {z | μ z ≤ 1},
        GammaFPP.HasC1CurveChart (frontier {z | μ z ≤ 1}) v := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.Analytic.NoCornerWedge, OAI.GammaFPP.HasC1CurveChart