Fixed-order bounds for the physical similarity coordinates

The inverse-coordinate jets are constructed from the actual inverse Jacobian. Their normalized values extend smoothly to the compact set q = 1, |eta| ≤ 1. Anisotropic homogeneity then gives a loss of at most one power of q per physical derivative.

@[reducible, inline]

abbrev NavierStokes.PhysicalCoordinateBounds.Point : Type

Point: an abbreviation for ℝ × (ℝ × ℝ).

Equations

• NavierStokes.PhysicalCoordinateBounds.Point = (ℝ × ℝ × ℝ)

noncomputable def NavierStokes.PhysicalCoordinateBounds.D (a : ℝ) : ℝ

D, given by (1 - a) / 2.

Equations

• NavierStokes.PhysicalCoordinateBounds.D a = (1 - a) / 2

noncomputable def NavierStokes.PhysicalCoordinateBounds.positiveTime : Set Point

Positive time, given by {p | 0 < p.1}.

Equations

• NavierStokes.PhysicalCoordinateBounds.positiveTime = {p : NavierStokes.PhysicalCoordinateBounds.Point | 0 < p.1}

noncomputable def NavierStokes.PhysicalCoordinateBounds.qCoord (a : ℝ) (p : Point) : ℝ

Q coord, given by coordinateQ a (p.1, p.2.2).

Equations

• NavierStokes.PhysicalCoordinateBounds.qCoord a p = NavierStokes.SimilarityCoordinates.coordinateQ a (p.1, p.2.2)

noncomputable def NavierStokes.PhysicalCoordinateBounds.inverseCoordinates (a : ℝ) (p : Point) : Point

Inverse coordinates, given by (qCoord a p, p.2).

Equations

• NavierStokes.PhysicalCoordinateBounds.inverseCoordinates a p = (NavierStokes.PhysicalCoordinateBounds.qCoord a p, p.2)

noncomputable def NavierStokes.PhysicalCoordinateBounds.inverseDifferential (a : ℝ) (y : Point) : Point →L[ℝ] Point

Inverse differential as an element of Point →L[ℝ] Point.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.PhysicalCoordinateBounds.inverseDifferential_apply (a : ℝ) (y v : Point) : (inverseDifferential a y) v = ((v.1 + 2 * y.2.2 * y.1 ^ a * v.2.2) / SimilarityCoordinates.scalarSlope a y.2.2 y.1, v.2)

theorem NavierStokes.PhysicalCoordinateBounds.positiveTime_isOpen : IsOpen positiveTime

theorem NavierStokes.PhysicalCoordinateBounds.qCoord_pos {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p ∈ positiveTime) : 0 < qCoord a p

theorem NavierStokes.PhysicalCoordinateBounds.qCoord_contDiffAt {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p ∈ positiveTime) : ContDiffAt ℝ (↑⊤) (qCoord a) p

theorem NavierStokes.PhysicalCoordinateBounds.inverseCoordinates_contDiffAt {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p ∈ positiveTime) : ContDiffAt ℝ (↑⊤) (inverseCoordinates a) p

theorem NavierStokes.PhysicalCoordinateBounds.inverseCoordinates_slope_pos {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p ∈ positiveTime) : 0 < SimilarityCoordinates.scalarSlope a p.2.2 (qCoord a p)

theorem NavierStokes.PhysicalCoordinateBounds.inverseCoordinates_hasFDerivAt {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p ∈ positiveTime) : HasFDerivAt (inverseCoordinates a) (inverseDifferential a (inverseCoordinates a p)) p

theorem NavierStokes.PhysicalCoordinateBounds.inverseDifferential_contDiffAt {a : ℝ} {y : Point} (hy : 0 < y.1) (hs : SimilarityCoordinates.scalarSlope a y.2.2 y.1 ≠ 0) : ContDiffAt ℝ (↑⊤) (inverseDifferential a) y

noncomputable def NavierStokes.PhysicalCoordinateBounds.inverseJet (a : ℝ) (g : Point → ℝ) (n : ℕ) : Point → Point [×n]→L[ℝ] ℝ

Actual inverse jets, computed by recursively differentiating through the inverse Jacobian. This definition assumes no derivative estimates.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.PhysicalCoordinateBounds.inverseJet a g 0 x✝ = (continuousMultilinearCurryFin0 ℝ NavierStokes.PhysicalCoordinateBounds.Point ℝ).symm (g x✝)

theorem NavierStokes.PhysicalCoordinateBounds.inverseJet_contDiffAt {a : ℝ} {g : Point → ℝ} {y : Point} (hy : 0 < y.1) (hs : SimilarityCoordinates.scalarSlope a y.2.2 y.1 ≠ 0) (hg : ContDiffAt ℝ (↑⊤) g y) (n : ℕ) : ContDiffAt ℝ (↑⊤) (inverseJet a g n) y

theorem NavierStokes.PhysicalCoordinateBounds.iteratedFDeriv_comp_inverse {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {g : Point → ℝ} (hg : ContDiffOn ℝ (↑⊤) g positiveTime) (n : ℕ) {p : Point} (hp : p ∈ positiveTime) : iteratedFDeriv ℝ n (g ∘ inverseCoordinates a) p = inverseJet a g n (inverseCoordinates a p)

noncomputable def NavierStokes.PhysicalCoordinateBounds.normalizedCompact (lo hi : ℝ) : Set Point

Normalized compact, given by ({1} : Set ℝ) ×ˢ (Icc lo hi ×ˢ Icc (-1 : ℝ) 1).

Equations

• NavierStokes.PhysicalCoordinateBounds.normalizedCompact lo hi = {1} ×ˢ Set.Icc lo hi ×ˢ Set.Icc (-1) 1

theorem NavierStokes.PhysicalCoordinateBounds.normalizedCompact_isCompact (lo hi : ℝ) : IsCompact (normalizedCompact lo hi)

theorem NavierStokes.PhysicalCoordinateBounds.normalized_slope_pos {a lo hi : ℝ} (ha : 0 < a) (ha1 : a < 1) {y : Point} (hy : y ∈ normalizedCompact lo hi) : 0 < SimilarityCoordinates.scalarSlope a y.2.2 y.1

theorem NavierStokes.PhysicalCoordinateBounds.exists_normalized_jet_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {g : Point → ℝ} (hg : ContDiffOn ℝ (↑⊤) g positiveTime) (lo hi : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ y ∈ normalizedCompact lo hi, ‖inverseJet a g n y‖ ≤ C

noncomputable def NavierStokes.PhysicalCoordinateBounds.dilation (a r : ℝ) : Point →L[ℝ] Point

The physical dilation: time and squared radius have weight one, while the axial variable has weight D = (1-a)/2.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.PhysicalCoordinateBounds.dilation_apply (a r : ℝ) (p : Point) : (dilation a r) p = (r * p.1, r * p.2.1, r ^ D a * p.2.2)

theorem NavierStokes.PhysicalCoordinateBounds.dilation_inv_cancel {r : ℝ} (hr : 0 < r) (a : ℝ) (p : Point) : (dilation a r) ((dilation a r⁻¹) p) = p

theorem NavierStokes.PhysicalCoordinateBounds.dilation_positive {r : ℝ} (hr : 0 < r) (a : ℝ) {p : Point} (hp : p ∈ positiveTime) : (dilation a r) p ∈ positiveTime

theorem NavierStokes.PhysicalCoordinateBounds.forwardScalar_dilation {r q : ℝ} (hr : 0 < r) (hq : 0 < q) (a z : ℝ) : SimilarityCoordinates.forwardScalar a (r ^ D a * z) (r * q) = r * SimilarityCoordinates.forwardScalar a z q

theorem NavierStokes.PhysicalCoordinateBounds.qCoord_dilation {a r : ℝ} (ha : 0 < a) (ha1 : a < 1) (hr : 0 < r) {p : Point} (hp : p ∈ positiveTime) : qCoord a ((dilation a r) p) = r * qCoord a p

theorem NavierStokes.PhysicalCoordinateBounds.inverseCoordinates_dilation {a r : ℝ} (ha : 0 < a) (ha1 : a < 1) (hr : 0 < r) {p : Point} (hp : p ∈ positiveTime) : inverseCoordinates a ((dilation a r) p) = (dilation a r) (inverseCoordinates a p)

noncomputable def NavierStokes.PhysicalCoordinateBounds.etaCoord (a : ℝ) (p : Point) : ℝ

Eta coord, given by p.2.2 / qCoord a p ^ D a.

Equations

• NavierStokes.PhysicalCoordinateBounds.etaCoord a p = p.2.2 / NavierStokes.PhysicalCoordinateBounds.qCoord a p ^ NavierStokes.PhysicalCoordinateBounds.D a

noncomputable def NavierStokes.PhysicalCoordinateBounds.xCoord (a : ℝ) (p : Point) : ℝ

X coord, given by p.2.1 / qCoord a p.

Equations

• NavierStokes.PhysicalCoordinateBounds.xCoord a p = p.2.1 / NavierStokes.PhysicalCoordinateBounds.qCoord a p

theorem NavierStokes.PhysicalCoordinateBounds.normalized_inverseCoordinates {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p ∈ positiveTime) : inverseCoordinates a ((dilation a (qCoord a p)⁻¹) p) = (1, xCoord a p, etaCoord a p)

theorem NavierStokes.PhysicalCoordinateBounds.normalized_mem {a lo hi : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p ∈ positiveTime) (hx : xCoord a p ∈ Set.Icc lo hi) : inverseCoordinates a ((dilation a (qCoord a p)⁻¹) p) ∈ normalizedCompact lo hi

theorem NavierStokes.PhysicalCoordinateBounds.iteratedFDeriv_comp_linear_open {F : Point → ℝ} {s : Set Point} (hs : IsOpen s) (hF : ContDiffOn ℝ (↑⊤) F s) (L : Point →L[ℝ] Point) (n : ℕ) {p : Point} (hp : L p ∈ s) : iteratedFDeriv ℝ n (F ∘ ⇑L) p = (iteratedFDeriv ℝ n F (L p)).compContinuousLinearMap fun (x : Fin n) => L

theorem NavierStokes.PhysicalCoordinateBounds.iteratedFDeriv_eq_of_eventuallyEq {F G : Point → ℝ} {p : Point} (heq : F =ᶠ[nhds p] G) (n : ℕ) : iteratedFDeriv ℝ n F p = iteratedFDeriv ℝ n G p

theorem NavierStokes.PhysicalCoordinateBounds.norm_dilation_le {r : ℝ} (hr : 0 ≤ r) (a : ℝ) : ‖dilation a r‖ ≤ max r (r ^ D a)

noncomputable def NavierStokes.PhysicalCoordinateBounds.scaleFactor (a qbig : ℝ) : ℝ

Scale factor, given by max 1 (qbig ^ (1 - D a)).

Equations

• NavierStokes.PhysicalCoordinateBounds.scaleFactor a qbig = max 1 (qbig ^ (1 - NavierStokes.PhysicalCoordinateBounds.D a))

theorem NavierStokes.PhysicalCoordinateBounds.scaleFactor_pos (a qbig : ℝ) : 0 < scaleFactor a qbig

theorem NavierStokes.PhysicalCoordinateBounds.norm_inverse_dilation_le {a q qbig : ℝ} (ha : 0 < a) (hq : 0 < q) (hqb : q ≤ qbig) : ‖dilation a q⁻¹‖ ≤ scaleFactor a qbig / q

theorem NavierStokes.PhysicalCoordinateBounds.pullback_contDiffOn {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {g : Point → ℝ} (hg : ContDiffOn ℝ (↑⊤) g positiveTime) : ContDiffOn ℝ (↑⊤) (g ∘ inverseCoordinates a) positiveTime

theorem NavierStokes.PhysicalCoordinateBounds.homogeneous_derivative_bound {a b : ℝ} (ha : 0 < a) (ha1 : a < 1) {g : Point → ℝ} (hg : ContDiffOn ℝ (↑⊤) g positiveTime) (hhom : ∀ r > 0, ∀ y ∈ positiveTime, g ((dilation a r) y) = r ^ b * g y) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ p ∈ positiveTime, qCoord a p ≤ qbig → xCoord a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (g ∘ inverseCoordinates a) p‖ ≤ C * qCoord a p ^ (b - ↑n)

A homogeneous smooth function of the inverse coordinates has loss at most n, independent of its degree. No derivative bound is an input.

noncomputable def NavierStokes.PhysicalCoordinateBounds.powerLift (b : ℝ) (y : Point) : ℝ

Power lift, given by y.1 ^ b.

Equations

• NavierStokes.PhysicalCoordinateBounds.powerLift b y = y.1 ^ b

noncomputable def NavierStokes.PhysicalCoordinateBounds.etaLift (a : ℝ) (y : Point) : ℝ

Eta lift, given by y.2.2 / y.1 ^ D a.

Equations

• NavierStokes.PhysicalCoordinateBounds.etaLift a y = y.2.2 / y.1 ^ NavierStokes.PhysicalCoordinateBounds.D a

noncomputable def NavierStokes.PhysicalCoordinateBounds.xLift (y : Point) : ℝ

X lift, given by y.2.1 / y.1.

Equations

• NavierStokes.PhysicalCoordinateBounds.xLift y = y.2.1 / y.1

theorem NavierStokes.PhysicalCoordinateBounds.powerLift_contDiffOn (b : ℝ) : ContDiffOn ℝ (↑⊤) (powerLift b) positiveTime

theorem NavierStokes.PhysicalCoordinateBounds.etaLift_contDiffOn (a : ℝ) : ContDiffOn ℝ (↑⊤) (etaLift a) positiveTime

theorem NavierStokes.PhysicalCoordinateBounds.xLift_contDiffOn : ContDiffOn ℝ (↑⊤) xLift positiveTime

theorem NavierStokes.PhysicalCoordinateBounds.powerLift_homogeneous (a b : ℝ) {r : ℝ} (hr : 0 < r) {y : Point} (hy : y ∈ positiveTime) : powerLift b ((dilation a r) y) = r ^ b * powerLift b y

theorem NavierStokes.PhysicalCoordinateBounds.etaLift_homogeneous (a : ℝ) {r : ℝ} (hr : 0 < r) {y : Point} (hy : y ∈ positiveTime) : etaLift a ((dilation a r) y) = r ^ 0 * etaLift a y

theorem NavierStokes.PhysicalCoordinateBounds.xLift_homogeneous (a : ℝ) {r : ℝ} (hr : 0 < r) {y : Point} (_hy : y ∈ positiveTime) : xLift ((dilation a r) y) = r ^ 0 * xLift y

theorem NavierStokes.PhysicalCoordinateBounds.power_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (b lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ p ∈ positiveTime, qCoord a p ≤ qbig → xCoord a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (fun (y : Point) => qCoord a y ^ b) p‖ ≤ C * qCoord a p ^ (b - ↑n)

Every fixed real power has the same derivative loss n; its degree remains explicitly in the weight q^(b-n).

theorem NavierStokes.PhysicalCoordinateBounds.q_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ p ∈ positiveTime, qCoord a p ≤ qbig → xCoord a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (qCoord a) p‖ ≤ C * qCoord a p ^ (1 - ↑n)

theorem NavierStokes.PhysicalCoordinateBounds.eta_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ p ∈ positiveTime, qCoord a p ≤ qbig → xCoord a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (etaCoord a) p‖ ≤ C * qCoord a p ^ (-↑n)

theorem NavierStokes.PhysicalCoordinateBounds.x_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ p ∈ positiveTime, qCoord a p ≤ qbig → xCoord a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (xCoord a) p‖ ≤ C * qCoord a p ^ (-↑n)

noncomputable def NavierStokes.PhysicalCoordinateBounds.timeReflection : Point ≃ₗᵢ[ℝ] Point

Time reflection, bundling toLinearEquiv, norm_map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.PhysicalCoordinateBounds.timeShift (p : Point) : Point

Time shift, given by (1 - p.1, p.2).

Equations

• NavierStokes.PhysicalCoordinateBounds.timeShift p = (1 - p.1, p.2)

theorem NavierStokes.PhysicalCoordinateBounds.timeShift_eq (p : Point) : timeShift p = (1, 0, 0) + timeReflection p

theorem NavierStokes.PhysicalCoordinateBounds.norm_iteratedFDeriv_timeShift (F : Point → ℝ) (n : ℕ) (p : Point) : ‖iteratedFDeriv ℝ n (F ∘ timeShift) p‖ = ‖iteratedFDeriv ℝ n F (timeShift p)‖

noncomputable def NavierStokes.PhysicalCoordinateBounds.physicalQ (a : ℝ) : Point → ℝ

Physical coordinates use (t,s,z). The exponent parameter here is a = 2h, so these definitions agree with the coordinates used by NaturalCore.

Equations

• NavierStokes.PhysicalCoordinateBounds.physicalQ a = NavierStokes.PhysicalCoordinateBounds.qCoord a ∘ NavierStokes.PhysicalCoordinateBounds.timeShift

noncomputable def NavierStokes.PhysicalCoordinateBounds.physicalEta (a : ℝ) : Point → ℝ

Physical eta, given by etaCoord a ∘ timeShift.

Equations

• NavierStokes.PhysicalCoordinateBounds.physicalEta a = NavierStokes.PhysicalCoordinateBounds.etaCoord a ∘ NavierStokes.PhysicalCoordinateBounds.timeShift

noncomputable def NavierStokes.PhysicalCoordinateBounds.physicalX (a : ℝ) : Point → ℝ

Physical X, given by xCoord a ∘ timeShift.

Equations

• NavierStokes.PhysicalCoordinateBounds.physicalX a = NavierStokes.PhysicalCoordinateBounds.xCoord a ∘ NavierStokes.PhysicalCoordinateBounds.timeShift

theorem NavierStokes.PhysicalCoordinateBounds.physicalQ_pos {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p.1 < 1) : 0 < physicalQ a p

theorem NavierStokes.PhysicalCoordinateBounds.physicalEta_abs_lt_one {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p.1 < 1) : |physicalEta a p| < 1

theorem NavierStokes.PhysicalCoordinateBounds.physicalQ_contDiffAt {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalQ a) p

theorem NavierStokes.PhysicalCoordinateBounds.physicalEta_contDiffAt {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalEta a) p

theorem NavierStokes.PhysicalCoordinateBounds.physicalX_contDiffAt {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : Point} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalX a) p

theorem NavierStokes.PhysicalCoordinateBounds.physical_power_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (b lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : Point), p.1 < 1 → physicalQ a p ≤ qbig → physicalX a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (fun (y : Point) => physicalQ a y ^ b) p‖ ≤ C * physicalQ a p ^ (b - ↑n)

theorem NavierStokes.PhysicalCoordinateBounds.physical_q_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : Point), p.1 < 1 → physicalQ a p ≤ qbig → physicalX a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (physicalQ a) p‖ ≤ C * physicalQ a p ^ (1 - ↑n)

theorem NavierStokes.PhysicalCoordinateBounds.physical_eta_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : Point), p.1 < 1 → physicalQ a p ≤ qbig → physicalX a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (physicalEta a) p‖ ≤ C * physicalQ a p ^ (-↑n)

theorem NavierStokes.PhysicalCoordinateBounds.physical_x_derivative_bound {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : Point), p.1 < 1 → physicalQ a p ≤ qbig → physicalX a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (physicalX a) p‖ ≤ C * physicalQ a p ^ (-↑n)

theorem NavierStokes.PhysicalCoordinateBounds.physical_coordinate_derivative_bounds {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : Point), p.1 < 1 → physicalQ a p ≤ qbig → physicalX a p ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (physicalQ a) p‖ ≤ C * physicalQ a p ^ (-↑n) ∧ ‖iteratedFDeriv ℝ n (physicalEta a) p‖ ≤ C * physicalQ a p ^ (-↑n) ∧ ‖iteratedFDeriv ℝ n (physicalX a) p‖ ≤ C * physicalQ a p ^ (-↑n)

One common constant controls all three coordinate functions, with the same explicit loss n. The constant depends only on the fixed geometry and the derivative order.

theorem NavierStokes.PhysicalCoordinateBounds.norm_fderiv_eq_iterated_one (F : Point → ℝ) (p : Point) : ‖fderiv ℝ F p‖ = ‖iteratedFDeriv ℝ 1 F p‖

theorem NavierStokes.PhysicalCoordinateBounds.physical_coordinate_fderiv_bounds {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (lo hi qbig : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : Point), p.1 < 1 → physicalQ a p ≤ qbig → physicalX a p ∈ Set.Icc lo hi → ‖fderiv ℝ (physicalQ a) p‖ ≤ C / physicalQ a p ∧ ‖fderiv ℝ (physicalEta a) p‖ ≤ C / physicalQ a p ∧ ‖fderiv ℝ (physicalX a) p‖ ≤ C / physicalQ a p