LeanPool.Clawristotle.LogBoundHelpers

theorem op_norm_bound_from_basis (L : (Fin 3 → ℝ) →L[ℝ] ℝ) {C : ℝ} (hC : 0 ≤ C) (bound : ∀ (i : Fin 3), ‖L (Pi.single i 1)‖ ≤ C) : ‖L‖ ≤ 3 * C

theorem mvt_test (g : (Fin 3 → ℝ) → ℝ) (hg_diff : Differentiable ℝ g) (Cg : ℝ) (Kg : ℕ) (hCg : 0 ≤ Cg) (bound : ∀ (v : Fin 3 → ℝ), ‖fderiv ℝ g v‖ ≤ Cg * (1 + ‖v‖) ^ Kg) (v : Fin 3 → ℝ) : |g v| ≤ |g 0| + Cg * (1 + ‖v‖) ^ (Kg + 1)

theorem log_f_zero_bound (f : Torus3 → (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) : ∃ C > 0, ∀ (x : Torus3), |Real.log (f x 0)| ≤ C

theorem log_bound_from_grad (f : Torus3 → (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth_v : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) (Cg : ℝ) (Kg : ℕ) (hGradBound : ∀ (x : Torus3) (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ (f x) v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f x v) : ∃ (C_log : ℝ) (K_log : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log