Calculus.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Derivatives of entropy and log-partition, and the nonlinear entropy barrier.

theorem OAI.MatchingEntropy.partition_hasDerivAt line 17
Source documentation
First derivative of a finite exponential partition function.
```
theorem partition_hasDerivAt {ι : Type*} [Fintype ι] (p a : ι → ℝ) (t : ℝ) :
    HasDerivAt (partition p a) (partition (fun i => p i*a i) a t) t := by
…
```
Mentions: OAI.MatchingEntropy.partition
theorem OAI.MatchingEntropy.logPartition_hasDerivAt line 26
Source documentation
The logarithmic partition derivative, with no infinite optimization or interchange of limits: only finite sums.
```
theorem logPartition_hasDerivAt {ι : Type*} [Fintype ι] {p : ι → ℝ}
    (hp : p ∈ probabilitySimplex ι) (a : ι → ℝ) (t : ℝ) :
    HasDerivAt (fun t => Real.log (partition p a t))
      (partition (fun i => p i*a i) a t / partition p a t) t :=
…
```
Mentions: OAI.MatchingEntropy.probabilitySimplex, OAI.MatchingEntropy.partition

theorem OAI.MatchingEntropy.logPartition_second line 33

Source documentation

The second derivative of log-partition at the base law is variance.

theorem logPartition_second {ι : Type*} [Fintype ι] {p : ι → ℝ}
    (hp : p ∈ probabilitySimplex ι) (a : ι → ℝ) :
    HasDerivAt (fun t => partition (fun i => p i*a i) a t / partition p a t)
      ((∑ i, p i*(a i)^2) - (∑ i, p i*a i)^2) 0 := by
…

Mentions: OAI.MatchingEntropy.probabilitySimplex, OAI.MatchingEntropy.partition

def OAI.MatchingEntropy.entropyLineD line 48
Source documentation
The explicit first derivative along a supported affine marginal path.
```
def entropyLineD {ι : Type*} [Fintype ι] (x v : ι → ℝ) (t : ℝ) : ℝ :=
…
```
theorem OAI.MatchingEntropy.entropy_line_hasDerivAt_at line 51
theorem OAI.MatchingEntropy.entropy_line_deriv_eventually line 70
theorem OAI.MatchingEntropy.entropyLineD_hasDerivAt line 84
theorem OAI.MatchingEntropy.entropy_line_second line 100
def OAI.MatchingEntropy.entropyBarrier line 107
def OAI.MatchingEntropy.entropyBarrierD line 108
theorem OAI.MatchingEntropy.entropyBarrier_hasDerivAt line 110
theorem OAI.MatchingEntropy.entropyBarrierD_hasDerivAt line 118

theorem OAI.MatchingEntropy.barrier_second_path line 127

Source documentation

Second derivative of the scalar barrier composed with any twice explicitly differentiable path.

theorem barrier_second_path {m : ℝ} (hm : m ≠ 0) {f fD : ℝ → ℝ} {fDD : ℝ}
    (hf : ∀ᶠ t in 𝓝 (0:ℝ), HasDerivAt f (fD t) t)
    (hDD : HasDerivAt fD fDD 0) :
    HasDerivAt (deriv (fun t => entropyBarrier m (f t)))
      (entropyBarrierD m (f 0)*fDD +
        (8*Real.exp (-f 0/m)/m)*(fD 0)^2) 0 := by
…

Mentions: OAI.MatchingEntropy.entropyBarrier, OAI.MatchingEntropy.entropyBarrierD

theorem OAI.MatchingEntropy.second_deriv_quadratic_adjustment line 151

Source documentation

A direct second-derivative calculation for the affine-law comparison path used below.

theorem second_deriv_quadratic_adjustment {f fD g gD : ℝ → ℝ} {fDD gDD c₀ c₁ v : ℝ}
    (hf : ∀ᶠ t in 𝓝 (0:ℝ), HasDerivAt f (fD t) t)
    (hg : ∀ᶠ t in 𝓝 (0:ℝ), HasDerivAt g (gD t) t)
    (hfD : HasDerivAt fD fDD 0) (hgD : HasDerivAt gD gDD 0) :
    HasDerivAt (deriv (fun t => f t+c₀+t*c₁+t^2*v-g t))
      (fDD+2*v-gDD) 0 := by
…

theorem OAI.MatchingEntropy.second_deriv_nonpos_of_local_max line 173
Source documentation
The necessary one-dimensional second-derivative test, also when the second derivative is defined by Lean's totalized derivative.
```
theorem second_deriv_nonpos_of_local_max {f : ℝ → ℝ} {x : ℝ}
    (hm : IsLocalMax f x) (hc : ContinuousAt f x) : deriv (deriv f) x ≤ 0 := by
…
```
theorem OAI.MatchingEntropy.entropy_line_eventually_hasDerivAt line 188
Source documentation
All first derivatives on a neighborhood, including boundary coordinates whose admissible direction is zero.
```
theorem entropy_line_eventually_hasDerivAt {ι : Type*} [Fintype ι] (x v : ι → ℝ)
    (hsupp : ∀ i, x i = 0 → v i = 0) :
    ∀ᶠ t : ℝ in 𝓝 0,
      HasDerivAt (fun t : ℝ => entropy (fun i => x i+t*v i)) (entropyLineD x v t) t := by
…
```
Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.entropyLineD
theorem OAI.MatchingEntropy.entropy_barrier_line_second line 202

theorem OAI.MatchingEntropy.entropy_second_variation line 216

Source documentation

The exact second variation along affine laws, proved solely by ordinary one-variable derivatives and the finite log-partition variance identity.

theorem entropy_second_variation {ι κ : Type*} [Fintype ι] [Fintype κ]
    (x v : ι → ℝ) (hsupp : ∀ i, x i = 0 → v i = 0)
    {p : κ → ℝ} (hp : p ∈ probabilitySimplex κ) (a : κ → ℝ)
    (hcenter : ∑ i, p i*a i = 0) {m : ℝ} (hm : m ≠ 0) (c₀ c₁ : ℝ)
    (hlocal : IsLocalMax (fun t => entropyBarrier m (entropy (fun i => x i+t*v i)) +
      c₀+t*c₁+t^2*(∑ i, p i*(a i)^2)-Real.log (partition p a t)) 0) :
    (8*Real.exp (-entropy x/m)-1)*(∑ i, (v i)^2/x i) +
      (8*Real.exp (-entropy x/m)/m)*(entropyLineD x v 0)^2 +
      (∑ i, p i*(a i)^2) ≤ 0 := by
…

Mentions: OAI.MatchingEntropy.probabilitySimplex, OAI.MatchingEntropy.entropyBarrier, OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.partition, OAI.MatchingEntropy.entropyLineD