Differentiability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Differentiability for Gamma weights

Theorem thm:gamma-differentiability of Strict convexity and differentiability of the planar exponential first-passage limit shape. The almost-sure passage-time limit is asserted for each fixed real direction.

theorem OAI.GammaFPP.gamma_differentiability line 20
Source documentation
Differentiability and regular C¹ boundary charts for planar Gamma first-passage percolation.
Distinct definitions of this name: ComparatorChallenges/GammaPassage.lean:107 (same statement text; different proof or body). Qualify references as OAI.GammaFPP.gamma_differentiability@path.
```
theorem gamma_differentiability : GammaDifferentiabilityTarget := by
…
```
Mentions: OAI.GammaFPP.GammaDifferentiabilityTarget