OrthogonalReduction

theorem OrthogonalReduction.local_stability {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (ι : H →ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)) (f0 : H) (hf0 : ‖ι f0‖ = 1) (M : ℝ) (hMpos : 0 < M) (hM : ∀ (g : H), inner ℂ g f0 = 0 → ‖g‖ ≤ M * MeasureTheory.lpNorm (fun (x : Ω) => ‖↑↑(ι (g + f0)) x‖ - ‖↑↑(ι f0) x‖) 2 μ) : ∃ δ > 0, ∃ M' > 0, ∀ (h : H), ‖h‖ ≤ δ → (inner ℂ h f0).im = 0 → ‖h‖ ≤ M' * MeasureTheory.lpNorm (fun (x : Ω) => ‖↑↑(ι (h + f0)) x‖ - ‖↑↑(ι f0) x‖) 2 μ