Nemytskii operators: ConverseImplication

Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).

theorem NemytskiiLebesgue.IsCaratheodory.growth_of_memLp_nemytskii_volume {m k : ℕ} {f : ℝ → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} (hf : IsCaratheodory f MeasureTheory.volume) {p : ENNReal} (h1p : 1 ≤ p) (hp : p < ⊤) {q : ENNReal} (h1q : 1 ≤ q) (hq : q < ⊤) (hpqf : ∀ (u : ℝ → EuclideanSpace ℝ (Fin m)), MeasureTheory.MemLp u p MeasureTheory.volume → MeasureTheory.MemLp (fun (x : ℝ) => f x (u x)) q MeasureTheory.volume) : ∃ (a : ℝ → ℝ), MeasureTheory.MemLp a q MeasureTheory.volume ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ᵐ (x : ℝ), ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f x ξ‖ ≤ |a x| + C * ‖ξ‖ ^ (p / q).toReal

theorem NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_volume_iff_growth {m k : ℕ} {f : ℝ → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} (hf : IsCaratheodory f MeasureTheory.volume) {p : ENNReal} (h1p : 1 ≤ p) (hp : p < ⊤) {q : ENNReal} (h1q : 1 ≤ q) (hq : q < ⊤) : (∀ (u : ℝ → EuclideanSpace ℝ (Fin m)), MeasureTheory.MemLp u p MeasureTheory.volume → MeasureTheory.MemLp (fun (x : ℝ) => f x (u x)) q MeasureTheory.volume) ↔ ∃ (a : ℝ → ℝ), MeasureTheory.MemLp a q MeasureTheory.volume ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ᵐ (x : ℝ), ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f x ξ‖ ≤ |a x| + C * ‖ξ‖ ^ (p / q).toReal