IndisputableMonolith.NavierStokes.PhiOptimalCascade

declarations in this module (10)

• def selfSimilarityDefect L24
• def simplifiedCascadeCost L28
• theorem selfSimilarityDefect_pos L31
• theorem selfSimilarityDefect_phi L36
• theorem simplifiedCascadeCost_phi L42
• theorem selfSimilarityDefect_eq_one_iff L47
• theorem positive_root_unique_above_one L59
• theorem simplifiedCascadeCost_eq_zero_iff L72
• theorem simplifiedCascadeCost_nonneg L84
• theorem phi_is_unique_optimal_ratio L90