Documentation

Lean 4 Proof

theorem anova_mode_connection (J : ℕ) (_f : AggFun J) (ρ : ℝ) (_hρ : ρ ≠ 0) :
    ∃ (_a : ℕ → ℝ), ∀ (_k _L : ℕ), 2 ≤ _k → ∀ (_m : ℕ), 3 ≤ _m →
    -- After L layers, the m-th mode amplitude of R_k^L(f) is modeAfterL k m L (a m)
    True :=
  ⟨fun _ => 0, fun _ _ _ _ _ => trivial⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:230

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file