ActionPenalty.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SharpLiebThirring.ActionProof.compact_penalty_bound line 27

Source documentation

The compact penalty argument, with no convergence of minimizers or chosen coefficients required.

lemma compact_penalty_bound {E : Type u35} [TopologicalSpace E] {K : Set E}
    (hK : IsCompact K) {f g : E → ℝ} (hf : Continuous f) (hg : Continuous g)
    (hg0 : ∀ x ∈ K, 0 ≤ g x) (hzero : ∀ x ∈ K, g x = 0 → f x ≤ 0)
    {η : ℝ} (hη : 0 < η) :
    ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ ε : ℝ, 0 < ε → ε ≤ ε₀ →
      ∀ x ∈ K, f x - g x / ε ≤ η := by
…

def OAI.SharpLiebThirring.ActionProof.actionDefect line 66
def OAI.SharpLiebThirring.ActionProof.constraintDefect line 71
lemma OAI.SharpLiebThirring.ActionProof.actionDefect_continuous line 75
lemma OAI.SharpLiebThirring.ActionProof.constraintDefect_continuous line 83
lemma OAI.SharpLiebThirring.ActionProof.constraintDefect_nonneg line 90
lemma OAI.SharpLiebThirring.ActionProof.constraintDefect_eq_zero_iff line 96

lemma OAI.SharpLiebThirring.ActionProof.matrix_compact_penalty line 113

Source documentation

Uniform compact penalty estimate for the matrix field and rank-one constraint.

lemma matrix_compact_penalty {σ δ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hδ : 0 < δ)
    (k : Fin N → ℝ)
    {K : Set (selfAdjoint (Matrix (Fin N) (Fin N) ℝ) × (Fin N → ℝ))} (hK : IsCompact K)
    {η : ℝ} (hη : 0 < η) :
    ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ ε : ℝ, 0 < ε → ε ≤ ε₀ → ∀ z ∈ K,
      actionDefect σ k z - constraintDefect σ δ k z / ε ≤ η := by
…

Mentions: OAI.SharpLiebThirring.ActionProof.actionDefect, OAI.SharpLiebThirring.ActionProof.constraintDefect

lemma OAI.SharpLiebThirring.PathProof.lower_gram_diagonal line 132

Source documentation

The initial row-sign orbit calculation, without assuming invertibility of any later matching solution.

lemma lower_gram_diagonal {C : Matrix (Fin N) (Fin N) ℝ} (hC : LowerTriangular C)
    {d : Fin N → ℝ} (hd : ∀ i, 0 < d i) (hgram : C * C.transpose = diagonal d) :
    (∀ i j, i ≠ j → C i j = 0) ∧ (∀ i, C i i ^ 2 = d i) := by
…

Mentions: OAI.SharpLiebThirring.LowerTriangular

lemma OAI.SharpLiebThirring.PathProof.lower_gram_initial_orbit line 170
def OAI.SharpLiebThirring.PathProof.triangularLinearInverse line 198
Source documentation
Explicit inverse for the initial linearized endpoint map, apart from its nonzero scalar factor -1/ε.
```
def triangularLinearInverse (c : Fin N → ℝ) (Z : Matrix (Fin N) (Fin N) ℝ) :
    Matrix (Fin N) (Fin N) ℝ :=
…
```
lemma OAI.SharpLiebThirring.PathProof.triangularLinearInverse_lower line 202
lemma OAI.SharpLiebThirring.PathProof.triangularLinearInverse_right line 207