HaarPolynomialMinimum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Maximum-principle signs for the genuine rotation Laplacian.

lemma OAI.InvariantIsing.haarPolynomialLaplacian_nonneg_at_min line 13

theorem OAI.InvariantIsing.haarPolynomial_parabolic_nonneg line 38

Source documentation

Compact-space parabolic comparison, with the spatial sign proved above.

theorem haarPolynomial_parabolic_nonneg {N : ℕ} {T : ℝ} (hT : 0 ≤ T)
    (p : ℝ → MatrixPolynomial N) (Wt : ℝ × SpecialOrthogonal N → ℝ)
    (hc : ContinuousOn (fun z : ℝ × SpecialOrthogonal N => haarPolynomialValue (p z.1) z.2)
      (Icc (0 : ℝ) T ×ˢ Set.univ))
    (hi : ∀ U : SpecialOrthogonal N, 0 ≤ haarPolynomialValue (p 0) U)
    (hd : ∀ t ∈ Ioc (0 : ℝ) T, ∀ U : SpecialOrthogonal N,
      HasDerivAt (fun s => haarPolynomialValue (p s) U) (Wt (t,U)) t)
    (hpde : ∀ t ∈ Ioc (0 : ℝ) T, ∀ U : SpecialOrthogonal N,
      haarPolynomialValue (haarPolynomialLaplacian N (p t)) U-
        haarPolynomialValue (p t) U ≤ Wt (t,U)) :
    ∀ t ∈ Icc (0 : ℝ) T, ∀ U : SpecialOrthogonal N,
      0 ≤ haarPolynomialValue (p t) U := by
…

Mentions: OAI.InvariantIsing.MatrixPolynomial, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.haarPolynomialValue, OAI.InvariantIsing.haarPolynomialLaplacian