pith. machine review for the scientific record. sign in
structure definition def or abbrev

VolcanicForcingAsJCostImpulseCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 238structure VolcanicForcingAsJCostImpulseCert where
 239  octave_period_eq_eight : octavePeriod = 8
 240  octave_period_minimal : ∀ {T : ℕ} (pass : Fin T → IndisputableMonolith.Patterns.Pattern 3),
 241    Function.Surjective pass → octavePeriod ≤ T
 242  impulse_nonneg : ∀ {vei : ℝ}, 0 < vei → 0 ≤ impulse_per_octave vei
 243  impulse_at_saturation_zero : impulse_per_octave vei_saturation = 0
 244  impulse_pinatubo_pos : 0 < impulse_per_octave (6 : ℝ)
 245  decay_mono : ∀ {vei : ℝ}, 0 < vei →
 246    ∀ (n m : ℕ), n ≤ m → 0 < impulse_per_octave vei →
 247      impulse_after_octaves vei m ≤ impulse_after_octaves vei n
 248

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.