DisplacementEstimate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Displacement forces a lower bound for the finite mean energy

The recursive identities concern the individual vectors, not the image of their mean under the Lipschitz map. Squared-norm convexity is applied to the mean of the differences of the images.

theorem OAI.ThompsonNonamenability.displacement_le_mean_energy line 23

Source documentation

The pointwise inequality obtained from the actual recursive colors.

theorem displacement_le_mean_energy {D : ℕ} (hD : 0 < D)
    (f : UnitBall E → UnitBall E) (L δ : ℝ)
    (_hL : 0 < L) (hδ : 0 < δ)
    (hLip : ∀ u v, ‖(f u : E) - f v‖ ≤ L * ‖(u : E) - v‖)
    (hDisp : ∀ u, δ ≤ ‖(f u : E) - u‖)
    (x z : Fin D → UnitBall E) (hrec : ∀ i, x i = f (z i)) :
    δ ^ 2 ≤ L ^ 2 * (D : ℝ)⁻¹ *
      ∑ i, ‖(z i : E) - (ballMean hD x : E)‖ ^ 2 := by
…

Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.ballMean