One quantitative coefficient budget for the actual source correction data. Every constant is independent of the jet order, truncation level and frequency. The assumptions are the original deformation and inverse-deformation derivative bounds; all stored coefficient and pressure estimates are derived from them.

The bounds stored in the actual recursive coefficient jet are controlled by the true word derivatives of its bounded-field translation orbit. A single enlargement of the coefficient radius gives fixed-base Sobolev bounds, independent of the jet truncation.

noncomputable def EulerCoefficientPath.coefficientDirections (i : Fin 4) : EulerSmoothLimit.Space

Coefficient directions, given by (standardDirection i).1.

Equations

• EulerCoefficientPath.coefficientDirections i = (EulerCylinderSobolev.standardDirection i).1

theorem EulerCoefficientPath.coefficientDirections_norm (i : Fin 4) : ‖coefficientDirections i‖ ≤ 1

theorem EulerCoefficientPath.translateCoefficientPath_zero {K : Type u_1} [TopologicalSpace K] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) : EulerMeanCoefficients.translateCoefficientPath A 0 = A

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathBounds1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathBounds2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathBounds2 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathBounds3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathBounds3 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathBounds4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathBounds4 = inferInstance

theorem EulerCoefficientPath.coefficientJet_boundLevel_le_words {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (s n : ℕ) (t : K) : EulerJetProductBounds.boundLevel P (coefficientJet P A hA s t) n ≤ EulerParameterWordGevrey.wordSum coefficientDirections (EulerMeanCoefficients.translateCoefficientPath A) n 0

theorem EulerCoefficientPath.coefficientJet_boundLevel_le_tensor {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (s n : ℕ) (t : K) : EulerJetProductBounds.boundLevel P (coefficientJet P A hA s t) n ≤ 4 ^ n * ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) 0‖

theorem EulerCoefficientPath.coefficientJet_block_le_words {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (s q n : ℕ) (t : K) : EulerH6Pressure.coefficientBlock P (coefficientJet P A hA s t) q n ≤ EulerParameterWordGevrey.coefficientBlock coefficientDirections q (EulerMeanCoefficients.translateCoefficientPath A) n 0

theorem EulerCoefficientPath.coefficientJet_block_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (s q : ℕ) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (t : K) : EulerH6Pressure.coefficientBlock P (coefficientJet P A hA s t) q n ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * EulerGevrey.majorant (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc) 0 n

Cutoff-independent weighted estimates for the actual coefficient jets. The positive-order coefficient normalization is paid once by a fixed coefficient radius, independent of the solution amplitude and grade.

def EulerCoefficientPath.normalizedCoefficientRadius (q : ℕ) (Rc C : ℝ) : ℝ

Normalized coefficient radius, given by `max 1 (sobolevCoefficientAmplitude (Fin 4) q Rc C)

• sobolevCoefficientRadius (Fin 4) Rc`.

Equations

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

theorem EulerCoefficientPath.normalizedCoefficientRadius_nonneg (q : ℕ) (Rc C : ℝ) (hRc : 0 ≤ Rc) : 0 ≤ normalizedCoefficientRadius q Rc C

theorem EulerCoefficientPath.amplitude_majorant_le_normalized (q : ℕ) (Rc C : ℝ) (hRc : 0 ≤ Rc) (n : ℕ) (hn : 1 ≤ n) : EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * EulerGevrey.majorant (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc) 0 n ≤ EulerGevrey.majorant (normalizedCoefficientRadius q Rc C) 0 n

theorem EulerCoefficientPath.coefficientJet_block_normalized {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (s q : ℕ) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (R : ℝ) (hR : normalizedCoefficientRadius q Rc C ≤ R) (n : ℕ) (hn : 1 ≤ n) (t : K) : EulerH6Pressure.coefficientBlock P (coefficientJet P A hA s t) q n ≤ R ^ n * ↑n.factorial ^ 2

theorem EulerCoefficientPath.coefficientJet_weighted_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (s q N : ℕ) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (ρ : ℝ) (hρ : 0 < ρ) (hsmall : ρ * EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ 1 / 2) (t : K) : EulerSobolevGevreyOperators.weightedCoefficient P (coefficientJet P A hA s t) q N ρ ≤ 2 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C

Actual coefficient-orbit bounds control the fixed H5/H6 pressure constants uniformly over all higher jet truncations.

theorem EulerCoefficientPath.boundLevel_le_block_zero (P : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} (J : EulerSpatialSobolevInverse.CoefficientJet P EulerCylinderSobolev.standardDirection s A) (q r : ℕ) (hr : r ≤ q) : EulerJetProductBounds.boundLevel P J r ≤ EulerH6Pressure.coefficientBlock P J q 0

theorem EulerCoefficientPath.coefficientJet_base_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (s q r : ℕ) (hr : r ≤ q) (t : K) : EulerJetProductBounds.boundLevel P (coefficientJet P A hA s t) r ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C

theorem EulerCoefficientPath.coefficientJet_restrictedPressure_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (s q b : ℕ) (hq : q ≤ s) (hqb : q ≤ b) (c : ℝ) (hc : 0 < c) (t : K) : (EulerH6Pressure.CoefficientJet.restrict (coefficientJet P A hA s t) q hq).pressureConstant c ≤ EulerCoefficientJetPressureBounds.pressureCost c (EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) b Rc C) q

Quantitative bounds for the actual packet coefficient towers.

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_block_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (s q n : ℕ) (t : ↑(Set.Icc 0 T)) : EulerH6Pressure.coefficientBlock P ((toCoefficientTower P A).jet s t) q n ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * EulerGevrey.majorant (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc) 0 n

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_base_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (s q r : ℕ) (hr : r ≤ q) (t : ↑(Set.Icc 0 T)) : EulerJetProductBounds.boundLevel P ((toCoefficientTower P A).jet s t) r ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_normalized_block (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (s q : ℕ) (R : ℝ) (hR : EulerCoefficientPath.normalizedCoefficientRadius q Rc C ≤ R) (n : ℕ) (hn : 1 ≤ n) (t : ↑(Set.Icc 0 T)) : EulerH6Pressure.coefficientBlock P ((toCoefficientTower P A).jet s t) q n ≤ R ^ n * ↑n.factorial ^ 2

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_weighted_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (s q N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (hsmall : ρ * EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ 1 / 2) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedCoefficient P ((toCoefficientTower P A).jet s t) q N ρ ≤ 2 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_pressure_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (s q b : ℕ) (hq : q ≤ s) (hqb : q ≤ b) (c : ℝ) (hc : 0 < c) (t : ↑(Set.Icc 0 T)) : (EulerH6Pressure.CoefficientJet.restrict ((toCoefficientTower P A).jet s t) q hq).pressureConstant c ≤ EulerCoefficientJetPressureBounds.pressureCost c (EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) b Rc C) q

structure EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] : Type

The coefficient part of the correction energy budget, uniformly at all orders and all Fourier scales with absolute value at most one.

• Rc : ℝ

  Rc of CorrectionCoefficientBudget, of type ℝ.

• M : ℝ

  M of CorrectionCoefficientBudget, of type ℝ.

• B : ℝ

  Bound parameter of CorrectionCoefficientBudget, of type ℝ.

• A0 : ℝ

  A0 of CorrectionCoefficientBudget, of type ℝ.

• A2 : ℝ

  A2 of CorrectionCoefficientBudget, of type ℝ.

• Rc_nonneg : 0 ≤ self.Rc
• M_one_le : 1 ≤ self.M
• B_nonneg : 0 ≤ self.B
• A0_nonneg : 0 ≤ self.A0
• A2_nonneg : 0 ≤ self.A2
• inverse_five (s : ℕ) (hs : 6 ≤ s) (t : ↑(Set.Icc 0 D.T)) : (EulerH6Pressure.CoefficientJet.restrict ((metricTower D P).jet s t) 5 ⋯).pressureConstant D.normalLower ≤ self.M
• inverse_six (s : ℕ) (hs : 6 ≤ s) (t : ↑(Set.Icc 0 D.T)) : (EulerH6Pressure.CoefficientJet.restrict ((metricTower D P).jet s t) 6 hs).pressureConstant D.normalLower ≤ self.M
• metric_derivatives (s : ℕ) (t : ↑(Set.Icc 0 D.T)) (l : ℕ) : 1 ≤ l → EulerH6Pressure.coefficientBlock P ((metricTower D P).jet s t) 6 l ≤ self.Rc ^ l * ↑l.factorial ^ 2
• metric_base (s : ℕ) (t : ↑(Set.Icc 0 D.T)) (r : ℕ) : r ≤ 6 → EulerJetProductBounds.boundLevel P ((metricTower D P).jet s t) r ≤ self.B
• linear (s N : ℕ) (ρ : ℝ) : 0 < ρ → 4 * self.M * (ρ * self.Rc) ≤ 1 → ∀ (t : ↑(Set.Icc 0 D.T)), EulerSobolevGevreyOperators.weightedCoefficient P ((linearTower D P).jet s t) 6 N ρ ≤ self.A0
• quadratic (κ : ℝ) : |κ| ≤ 1 → ∀ (s N : ℕ) (ρ : ℝ), 0 < ρ → 4 * self.M * (ρ * self.Rc) ≤ 1 → ∀ (t : ↑(Set.Icc 0 D.T)), ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient P ((quadraticTower D P κ i).jet s t) 6 N ρ ≤ self.A2

def EulerPacketCorrectionCoefficients.correctionMetricEnvelope (R CI : ℝ) : ℝ

Correction metric envelope, given by sobolevCoefficientAmplitude (Fin 4) 6 (4*R) (3*CI*CI).

Equations

• EulerPacketCorrectionCoefficients.correctionMetricEnvelope R CI = EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 (4 * R) (3 * CI * CI)

def EulerPacketCorrectionCoefficients.correctionLinearEnvelope (R C1 CI : ℝ) : ℝ

Correction linear envelope, given by 2*sobolevCoefficientAmplitude (Fin 4) 6 (4*R) (6*CI*C1).

Equations

• EulerPacketCorrectionCoefficients.correctionLinearEnvelope R C1 CI = 2 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 (4 * R) (6 * CI * C1)

def EulerPacketCorrectionCoefficients.correctionQuadraticEnvelope (R C0 CI : ℝ) : ℝ

Correction quadratic envelope, given by 6*sobolevCoefficientAmplitude (Fin 4) 6 (4*R) (3*CI*(C0*R)).

Equations

• EulerPacketCorrectionCoefficients.correctionQuadraticEnvelope R C0 CI = 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 (4 * R) (3 * CI * (C0 * R))

def EulerPacketCorrectionCoefficients.correctionCoefficientRadius (R CI : ℝ) : ℝ

Correction coefficient radius, given by max 1 (max (normalizedCoefficientRadius 6 (4*R) (3*CI*CI)) (sobolevCoefficientRadius (Fin 4) (4*R))).

Equations

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

noncomputable def EulerPacketCorrectionCoefficients.correctionPressureEnvelope (c R CI : ℝ) : ℝ

Correction pressure envelope, given by max 1 (max (pressureCost c (correctionMetricEnvelope R CI) 5) (pressureCost c (correctionMetricEnvelope R CI) 6)).

Equations

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

noncomputable def EulerPacketCorrectionCoefficients.correctionCoefficientBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (R C0 C1 CI : ℝ) (hR : 0 ≤ R) (hC0 : 0 ≤ C0) (hC1 : 0 ≤ C1) (hCI : 0 ≤ CI) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) (hF1 : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C1 * EulerGevrey.majorant R 0 n) (hFI : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ CI * EulerGevrey.majorant R 0 n) : CorrectionCoefficientBudget D P

All coefficient hypotheses of the correction energy estimate, derived from genuine source spatial jets. The radius condition is the same one used by the projected inverse, rather than a separate cutoff-dependent restriction.

Equations

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