OAI/Analysis/AffineBernstein/DualDetBarrier.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.dualCutoff line 19
2. def OAI.AffineBernstein.dualDetBarrier line 21
3. lemma OAI.AffineBernstein.dirDeriv_dualCutoff line 24
4. lemma OAI.AffineBernstein.hessian_dualCutoff line 30
5. lemma OAI.AffineBernstein.contDiffOn_dualCutoff line 35
6. lemma OAI.AffineBernstein.inverseHessianPair_dualCutoff line 39
7. lemma OAI.AffineBernstein.inverseHessianTrace_log_function line 47
8. lemma OAI.AffineBernstein.contDiffOn_dualDetBarrier line 65
9. lemma OAI.AffineBernstein.dualDetBarrier_critical_gradient line 73
10. lemma OAI.AffineBernstein.inverseHessianTrace_dualDetBarrier line 99
11. lemma OAI.AffineBernstein.inverseHessianPair_position_le_trace line 124
12. lemma OAI.AffineBernstein.dualDetBarrier_peak_identity line 140

    Source documentation

    Exact pulled-back dual equation at a critical point. The Q term cancels for β=n+2, retaining the original (n+1)/(n+2) exponent.

    lemma dualDetBarrier_peak_identity {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
        {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
        (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
        (h : ℝ) (hneg : ∀ x ∈ Ω, dualCutoff u h x < 0) {x : Space n} (hx : x ∈ Ω) (γ : ℝ)
        (hmax : IsLocalMax (dualDetBarrier u h ((n:ℝ)+2) γ) x) :
        inverseHessianTrace u (dualDetBarrier u h ((n:ℝ)+2) γ) x =
          γ*(hessian u x)⁻¹.trace - (((n:ℝ)+1)/((n:ℝ)+2))*γ^2 *
            inverseHessianPair u positionEnergy positionEnergy x +
          ((n:ℝ)*((n:ℝ)+2) - γ*(n:ℝ)*positionSquared x)/dualCutoff u h x := by
    …

    Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.dualCutoff, OAI.AffineBernstein.dualDetBarrier, OAI.AffineBernstein.inverseHessianTrace, OAI.AffineBernstein.inverseHessianPair, OAI.AffineBernstein.positionEnergy, OAI.AffineBernstein.positionSquared