Mathematics, from question to proof.

lean/MathProofs/StrictBinding.lean:531 · theorem strict_binding

theorem strict_binding (hβ : 0 < β) (hγ : 0 < γ) {m μ : ℝ} (hm : 0 < m) (hmB : m ≤ mB β γ k)
    (hμ : 0 < μ) (hμm : μ < m) :
    Imin β γ k m < Imin β γ k μ + Imin β γ k (m - μ) :=

Representative proof step from source

have h1 := gap (k := k) hβ hγ hμ hμm (by linarith)

The first code block is the theorem statement with its hypotheses. The full source contains its Lean proof body and dependencies.

lean/MathProofs/WholeSpaceMinimizers.lean:1492 · theorem exists_minimizer

theorem exists_minimizer (hβ : 0 < β) (hγ : 0 < γ) {m : ℝ} (hm : 0 < m)
    (hmB : m ≤ StrictBinding.mB β γ k) :
    ∃ U : H2 2, M U = m ∧ energy β γ k U = Imin β γ k m :=

Representative proof step from source

obtain ⟨-, -, -, U, hUm, hUE, -⟩ := compactness hβ hγ hm hmB hum hE

The first code block is the theorem statement with its hypotheses. The full source contains its Lean proof body and dependencies.

lean/MathProofs/CubicQuinticFlow.lean:926 · theorem global_wellposed

theorem global_wellposed (hγ : 0 < γ) (u₀ : H2 2) :
    ∃! u : ℝ → H2 2, IsSolution β γ k u ∧ u 0 = u₀ :=

Representative proof step from source

obtain ⟨W, hW0, hW⟩ := exists_global (β := β) (γ := γ) (k := k) hγ (H2.toSp u₀)

The first code block is the theorem statement with its hypotheses. The full source contains its Lean proof body and dependencies.

lean/MathProofs/OrbitalStability.lean:256 · theorem orbital_stability

theorem orbital_stability (hβ : 0 < β) (hγ : 0 < γ) {m : ℝ} (hm : 0 < m)
    (hmB : m ≤ StrictBinding.mB β γ k) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ > 0, ∀ u : ℝ → H2 2, IsSolution β γ k u → distX (u 0) (Gset β γ k m) < δ →
      BddAbove (Set.range fun t => distX (u t) (Gset β γ k m)) ∧
      ⨆ t, distX (u t) (Gset β γ k m) < ε :=

Representative proof step from source

obtain ⟨δ, hδ, hcore⟩ := stable_core hβ hγ hm hmB (half_pos hε)

The first code block is the theorem statement with its hypotheses. The full source contains its Lean proof body and dependencies.

lean/MathProofs/V18Identifiability.lean:32 · theorem observed_local_level_set

theorem observed_local_level_set (alpha : ℝ) (ha : 0 ≤ alpha) :
    HasTwentyDimensionalLocalFiber alpha :=

Representative proof step from source

exists_c1_level_set_chart observed (frozen alpha 5) (jacobian (frozen alpha 5))

The first code block is the theorem statement with its hypotheses. The full source contains its Lean proof body and dependencies.

lean/MathProofs/ManifoldScalarMetric.lean:247 · theorem main

theorem main (ψ : M → ℂ) (_hψ : ContMDiff I 𝓘(ℝ, ℂ) 1 ψ)
    (h4 : Module.finrank ℝ E = 4) (p : M) :
    (tensor I ψ p).IsSymm ∧
    (∀ v, 0 ≤ tensor I ψ p v v) ∧
    LinearMap.ker (tensor I ψ p) =
      LinearMap.ker (mfderiv I 𝓘(ℝ, ℂ) ψ p).toLinearMap ∧
    Module.finrank ℝ (LinearMap.range (tensor I ψ p)) ≤ 2 ∧
    2 ≤ Module.finrank ℝ (LinearMap.ker (tensor I ψ p)) ∧
    ¬ (tensor I ψ p).Nondegenerate :=

Representative proof step from source

exact ⟨gram_symmetric _, gram_nonnegative _, gram_ker _, gram_rank_le_two _,
    gram_nullity _ h4, gram_degenerate _ h4⟩

The first code block is the theorem statement with its hypotheses. The full source contains its Lean proof body and dependencies.