ScalarTransportBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The transported bump estimate used in each compact detector block. All flow estimates here follow from the same two variational equations.

theorem OAI.ForcedComputation.VelocityDetector.inverse_second_variation_sharp line 13

theorem OAI.ForcedComputation.VelocityDetector.hessian_trace_bound line 31

Source documentation

The trace costs a factor of two in the planar Euclidean norm.

theorem hessian_trace_bound (f : EuclideanPlane → ℝ) (x : EuclideanPlane)
    {B : ℝ} (hB : ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ B) :
    |∑ j : Fin 2, fderiv ℝ (fderiv ℝ f) x
      (EuclideanSpace.single j 1) (EuclideanSpace.single j 1)| ≤ 2 * B := by
…

Mentions: OAI.ForcedComputation.EuclideanPlane

theorem OAI.ForcedComputation.VelocityDetector.inverse_flow_block_bounds line 52

Source documentation

A block runs at most n periods. The inverse-flow Hessian has the polynomial prefactor needed for the manuscript's exact rational scale.

theorem inverse_flow_block_bounds {V : ℝ → EuclideanPlane → EuclideanPlane}
    {Ψ : ℝ → ℝ → EuclideanPlane → EuclideanPlane} (hv : EuclideanVariations V Ψ)
    (L n : ℕ) (hL : 0 < L)
    (hb₁ : ∀ a x, ‖fderiv ℝ (V a) x‖ ≤ (L : ℝ))
    (hb₂ : ∀ a x, ‖fderiv ℝ (fderiv ℝ (V a)) x‖ ≤ (L : ℝ))
    (a : ℝ) (x : EuclideanPlane) {s : ℝ} (hs : 0 ≤ s) (hsn : s ≤ n) :
    ‖fderiv ℝ (Ψ a (-s)) x‖ ≤ (expansion L : ℝ) ^ n ∧
    ‖fderiv ℝ (fderiv ℝ (Ψ a (-s))) x‖ ≤
      (n : ℝ) * L * (expansion L : ℝ) ^ (3 * n) := by
…

Mentions: OAI.ForcedComputation.EuclideanPlane, OAI.ForcedComputation.EuclideanVariations, OAI.ForcedComputation.VelocityDetector.expansion

theorem OAI.ForcedComputation.VelocityDetector.transported_hessian_bound line 80

Source documentation

The chain rule gives exactly the scale used in the detector, before multiplying by the dimension to take a Laplacian.

theorem transported_hessian_bound {g : EuclideanPlane → ℝ}
    {φ : EuclideanPlane → EuclideanPlane} (hg : ContDiff ℝ ∞ g)
    (hφ : ContDiff ℝ ∞ φ) (x : EuclideanPlane) (C L n : ℕ)
    {b : ℝ} (hb : 0 < b) (hb₁ : b ≤ 1)
    (hg₁ : ‖fderiv ℝ g (φ x)‖ ≤ (C : ℝ) * b⁻¹)
    (hg₂ : ‖fderiv ℝ (fderiv ℝ g) (φ x)‖ ≤ (C : ℝ) * b⁻¹ ^ 2)
    (hφ₁ : ‖fderiv ℝ φ x‖ ≤ (expansion L : ℝ) ^ n)
    (hφ₂ : ‖fderiv ℝ (fderiv ℝ φ) x‖ ≤
      (n : ℝ) * L * (expansion L : ℝ) ^ (3 * n)) :
    ‖fderiv ℝ (fderiv ℝ (g ∘ φ)) x‖ ≤
      (C : ℝ) * b⁻¹ ^ 2 * (1 + (n : ℝ) * L) * (expansion L : ℝ) ^ (3 * n) := by
…

Mentions: OAI.ForcedComputation.EuclideanPlane, OAI.ForcedComputation.VelocityDetector.expansion