Convex
Results named in Tau Ceti's TauCeti.Analysis.Convex modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe Aleksandrov maximum principle#
Let Ω be a bounded open convex subset of a real inner
product space E of finite dimension n ≥ 1, and let u be convex on Ω, continuous on its
closure, and nonnegative on its frontier. Then at every x₀ ∈ Ω,
max (-u x₀) 0 ^ n * μ (ball 0 1) ≤ 2 ^ (n + 1) * diam Ω ^ (n - 1) * dist(x₀, ∂Ω) * MA_u(Ω),
where dist(x₀, ∂Ω) is the distance from x₀ to the complement of Ω and MA_u is the
Aleksandrov Monge–Ampère measure of u (extended by ⊤ off Ω) with respect to the additive
Haar measure μ. When MA_u(Ω) is finite, this bounds the negative part max (-u x₀) 0 above
on Ω and shows that max (-u x₀) 0 = O(dist(x₀, ∂Ω) ^ (1 / n)) as x₀ approaches the
boundary.
TauCeti.ofReal_neg_pow_mul_addHaar_ball_le_mul_mongeAmpereMeasure.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] {Ω : Set E} {u : E → ℝ} [Nontrivial E] (μ : MeasureTheory.Measure E)
[μ.IsAddHaarMeasure] [DecidablePred fun x => x ∈ Ω] (hΩo : IsOpen Ω) (hΩ : Bornology.IsBounded Ω)
(hu : ConvexOn ℝ Ω u) (hc : ContinuousOn u (closure Ω)) (hfr : ∀ x ∈ frontier Ω, 0 ≤ u x) {x₀ : E}
(hx₀ : x₀ ∈ Ω) :
ENNReal.ofReal (-u x₀) ^ Module.finrank ℝ E * μ (Metric.ball 0 1) ≤
2 ^ (Module.finrank ℝ E + 1) *
ENNReal.ofReal (Metric.diam Ω ^ (Module.finrank ℝ E - 1) * Metric.infDist x₀ Ωᶜ) *
(TauCeti.mongeAmpereMeasure μ fun x => if x ∈ Ω then ↑(u x) else ⊤) Ω
Lean
Formalized in Tau Ceti as TauCeti.ofReal_neg_pow_mul_addHaar_ball_le_mul_mongeAmpereMeasure.
Sources
Uses 2 · Used by 1
TheoremAlexandrov's theorem#
Let f : E → EReal be convex (convex real epigraph, never ⊥) on a
finite-dimensional real inner product space with an additive Haar measure μ, and let
F x = (f x).toReal. At μ-almost every point x of the effective domain, F has a
second-order Taylor expansion
F x' = F x + ⟪∇F x, x' - x⟫ + ⟪A (x' - x), x' - x⟫ / 2 + o(‖x' - x‖ ^ 2)
with a positive operator A, the only positive operator giving such an expansion.
TauCeti.ae_existsUnique_isPositive_isLittleO.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f : E → EReal}
(hf : Convex ℝ {p | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) :
∀ᵐ (x : E) ∂μ,
f x ≠ ⊤ →
∃! A,
A.IsPositive ∧
(fun x' =>
(f x').toReal - (f x).toReal -
inner ℝ (gradient (fun x' => (f x').toReal) x) (x' - x) -
inner ℝ (A (x' - x)) (x' - x) / 2) =o[nhds x]
fun x' => ‖x' - x‖ ^ 2
Lean
Formalized in Tau Ceti as TauCeti.ae_existsUnique_isPositive_isLittleO.
Other forms
Alexandrov's theorem for a real convex function. Formalized in Tau Ceti as ConvexOn.ae_existsUnique_isPositive_isLittleO.
ConvexOn.ae_existsUnique_isPositive_isLittleO.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : Set E} {u : E → ℝ} (hu : ConvexOn ℝ Ω u) :
∀ᵐ (x : E) ∂μ,
x ∈ Ω →
DifferentiableAt ℝ u x ∧
∃! A,
A.IsPositive ∧
(fun x' =>
u x' - u x - inner ℝ (gradient u x) (x' - x) -
inner ℝ (A (x' - x)) (x' - x) / 2) =o[nhds x]
fun x' => ‖x' - x‖ ^ 2
Alexandrov's theorem for the subdifferential. Formalized in Tau Ceti as TauCeti.ae_existsUnique_isPositive_forall_mem_subdifferential_norm_sub_le.
TauCeti.ae_existsUnique_isPositive_forall_mem_subdifferential_norm_sub_le.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f : E → EReal}
(hf : Convex ℝ {p | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) :
∀ᵐ (x : E) ∂μ,
f x ≠ ⊤ →
∃! A,
A.IsPositive ∧
∀ ε > 0,
∀ᶠ (x' : E) in nhds x,
∀ y' ∈ TauCeti.subdifferential (innerₗ E) f x',
‖y' - gradient (fun x' => (f x').toReal) x - A (x' - x)‖ ≤ ε * ‖x' - x‖
Sources
TheoremThe Fenchel–Moreau theorem#
Let the pairing B represent every continuous linear
functional on the locally convex space E. If f : E → EReal has convex real epigraph, is lower
semicontinuous and never takes the value ⊥, then f equals its biconjugate f⋆⋆, the second
conjugate being taken for the transposed pairing.
TauCeti.fenchelConjugate_flip_fenchelConjugate_eq.{u_1, u_2} {E : Type u_1} [AddCommGroup E]
[_root_.Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E] {f : E → EReal} {F : Type u_2} [AddCommGroup F] [_root_.Module ℝ F]
{B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : ∀ (ℓ : E →L[ℝ] ℝ), ∃ y, ∀ (x : E), (B x) y = ℓ x)
(hf : Convex ℝ {p | f p.1 ≤ ↑p.2}) (hlsc : LowerSemicontinuous f) (hbot : ∀ (x : E), f x ≠ ⊥) :
TauCeti.fenchelConjugate B.flip (TauCeti.fenchelConjugate B f) = f
Lean
Formalized in Tau Ceti as TauCeti.fenchelConjugate_flip_fenchelConjugate_eq.
Other forms
The Fenchel–Moreau theorem on a complete real inner product space. Formalized in Tau Ceti as TauCeti.fenchelConjugate_innerₗ_fenchelConjugate_innerₗ.
TauCeti.fenchelConjugate_innerₗ_fenchelConjugate_innerₗ.{u_2} {G : Type u_2} [NormedAddCommGroup G]
[InnerProductSpace ℝ G] [CompleteSpace G] {f : G → EReal} (hf : Convex ℝ {p | f p.1 ≤ ↑p.2})
(hlsc : LowerSemicontinuous f) (hbot : ∀ (x : G), f x ≠ ⊥) :
TauCeti.fenchelConjugate (innerₗ G) (TauCeti.fenchelConjugate (innerₗ G) f) = f
The Fenchel–Moreau theorem, with its converse. Formalized in Tau Ceti as TauCeti.fenchelConjugate_flip_fenchelConjugate_eq_iff.
TauCeti.fenchelConjugate_flip_fenchelConjugate_eq_iff.{u_1, u_2} {E : Type u_1} [AddCommGroup E]
[_root_.Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E] {f : E → EReal} {F : Type u_2} [AddCommGroup F] [_root_.Module ℝ F]
{B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : ∀ (ℓ : E →L[ℝ] ℝ), ∃ y, ∀ (x : E), (B x) y = ℓ x)
(hBc : ∀ (y : F), Continuous fun x => (B x) y) :
TauCeti.fenchelConjugate B.flip (TauCeti.fenchelConjugate B f) = f ↔
Convex ℝ {p | f p.1 ≤ ↑p.2} ∧ LowerSemicontinuous f ∧ ((∀ (x : E), f x ≠ ⊥) ∨ f = ⊥)
Sources
Uses 1
TheoremThe Fenchel–Young inequality#
The Fenchel–Young inequality in additive form, ⟪x, y⟫ ≤ f x + f⋆ y, valid whenever
neither summand is ⊥; the second summand is ⊥ only when f ≡ ⊤.
TauCeti.le_add_fenchelConjugate.{u_1, u_2} {E : Type u_1} {F : Type u_2} [AddCommMonoid E]
[_root_.Module ℝ E] [AddCommMonoid F] [_root_.Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal}
{x : E} {y : F} (hx : f x ≠ ⊥) (hy : TauCeti.fenchelConjugate B f y ≠ ⊥) :
↑((B x) y) ≤ f x + TauCeti.fenchelConjugate B f y
Lean
Formalized in Tau Ceti as TauCeti.le_add_fenchelConjugate.
Other forms
The Fenchel–Young inequality, in the form that holds with no hypothesis. Formalized in Tau Ceti as TauCeti.sub_le_fenchelConjugate.
TauCeti.sub_le_fenchelConjugate.{u_1, u_2} {E : Type u_1} {F : Type u_2} [AddCommMonoid E]
[_root_.Module ℝ E] [AddCommMonoid F] [_root_.Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal)
(x : E) (y : F) : ↑((B x) y) - f x ≤ TauCeti.fenchelConjugate B f y
Sources
Used by 8
TheoremGrothendieck's compactness lemma#
A totally bounded subset of a real seminormed space lies
in the closed convex hull of the range of a sequence tending to 0.
TotallyBounded.exists_tendsto_zero_subset_closure_convexHull.{u_1} {E : Type u_1}
[SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : TotallyBounded s) :
∃ x, Filter.Tendsto x Filter.atTop (nhds 0) ∧ s ⊆ closure ((convexHull ℝ) (Set.range x))
Lean
Formalized in Tau Ceti as TotallyBounded.exists_tendsto_zero_subset_closure_convexHull.
Sources
TheoremJensen's theorem#
On a convex subset of a real topological vector space, a continuous function that is midpoint convex is convex.
TauCeti.convexOn_of_midpoint.{u_1} {E : Type u_1} [AddCommGroup E] [_root_.Module ℝ E]
[TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {f : E → ℝ}
(hs : Convex ℝ s) (hf : ContinuousOn f s)
(h : ∀ x ∈ s, ∀ y ∈ s, f (midpoint ℝ x y) ≤ (f x + f y) / 2) : ConvexOn ℝ s f
TheoremLebesgue decomposition of the Monge–Ampère measure#
Let f : E → EReal be convex
(convex real epigraph, never ⊥) with D the interior of its effective domain, and let H x be,
for almost every x ∈ D, a first-order expansion of the subdifferential of f at x (the
Alexandrov Hessian, see rnDeriv_mongeAmpereMeasure_ae_eq). Then for every additive Haar measure
μ, the Aleksandrov Monge–Ampère measure splits as MA_f = (MA_f)ˢ + det (H x) dx on D, where
(MA_f)ˢ is the part singular with respect to μ. So the Alexandrov Hessian determines exactly
the absolutely continuous part of MA_f. This is the case g = 1 of
mongeAmpereMeasure_withDensity_eq_singularPart_add_withDensity.
TauCeti.mongeAmpereMeasure_eq_singularPart_add_withDensity.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal}
[MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
(hf : Convex ℝ {p | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {H : E → E →L[ℝ] E}
(hH :
∀ᵐ (x : E) ∂μ,
x ∈ interior {x | f x ≠ ⊤} →
∃ y,
∀ ε > 0,
∀ᶠ (x' : E) in nhds x,
∀ y' ∈ TauCeti.subdifferential (innerₗ E) f x',
‖y' - y - (H x) (x' - x)‖ ≤ ε * ‖x' - x‖) :
TauCeti.mongeAmpereMeasure μ f =
(TauCeti.mongeAmpereMeasure μ f).singularPart μ +
(μ.restrict (interior {x | f x ≠ ⊤})).withDensity fun x => ENNReal.ofReal (H x).det
Lean
Formalized in Tau Ceti as TauCeti.mongeAmpereMeasure_eq_singularPart_add_withDensity.
Other forms
Lebesgue decomposition of the Monge–Ampère measure, with the Alexandrov Hessian. Formalized in Tau Ceti as TauCeti.exists_mongeAmpereMeasure_eq_singularPart_add_withDensity.
TauCeti.exists_mongeAmpereMeasure_eq_singularPart_add_withDensity.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal}
[MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
(hf : Convex ℝ {p | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) :
∃ H,
(∀ᵐ (x : E) ∂μ,
f x ≠ ⊤ →
(H x).IsPositive ∧
∀ ε > 0,
∀ᶠ (x' : E) in nhds x,
∀ y' ∈ TauCeti.subdifferential (innerₗ E) f x',
‖y' - gradient (fun x' => (f x').toReal) x - (H x) (x' - x)‖ ≤ ε * ‖x' - x‖) ∧
TauCeti.mongeAmpereMeasure μ f =
(TauCeti.mongeAmpereMeasure μ f).singularPart μ +
(μ.restrict (interior {x | f x ≠ ⊤})).withDensity fun x => ENNReal.ofReal (H x).det
Lebesgue decomposition of the weighted Monge–Ampère measure. Formalized in Tau Ceti as TauCeti.mongeAmpereMeasure_withDensity_eq_singularPart_add_withDensity.
TauCeti.mongeAmpereMeasure_withDensity_eq_singularPart_add_withDensity.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal}
[MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
(hf : Convex ℝ {p | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {H : E → E →L[ℝ] E}
(hH :
∀ᵐ (x : E) ∂μ,
x ∈ interior {x | f x ≠ ⊤} →
∃ y,
∀ ε > 0,
∀ᶠ (x' : E) in nhds x,
∀ y' ∈ TauCeti.subdifferential (innerₗ E) f x',
‖y' - y - (H x) (x' - x)‖ ≤ ε * ‖x' - x‖)
{g : E → ENNReal} (hg : Measurable g) :
TauCeti.mongeAmpereMeasure (μ.withDensity g) f =
(TauCeti.mongeAmpereMeasure (μ.withDensity g) f).singularPart μ +
(μ.restrict (interior {x | f x ≠ ⊤})).withDensity fun x =>
ENNReal.ofReal (H x).det * g (gradient (fun x' => (f x').toReal) x)
Sources
TheoremRademacher's theorem for extended-real convex functions#
Let f : E → EReal have convex
real epigraph and never take the value ⊥, on a finite-dimensional real normed space E with an
additive Haar measure μ. Then at μ-almost every point x of the effective domain, f is
finite on a neighbourhood of x and its real representative x ↦ (f x).toReal is
differentiable at x.
TauCeti.ae_eventually_ne_top_and_differentiableAt_toReal.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {f : E → EReal} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hf : Convex ℝ {p | f p.1 ≤ ↑p.2})
(hbot : ∀ (x : E), f x ≠ ⊥) :
∀ᵐ (x : E) ∂μ,
f x ≠ ⊤ → (∀ᶠ (x' : E) in nhds x, f x' ≠ ⊤) ∧ DifferentiableAt ℝ (fun x' => (f x').toReal) x
Lean
Formalized in Tau Ceti as TauCeti.ae_eventually_ne_top_and_differentiableAt_toReal.
Sources
Uses 1 · Used by 6
TheoremRado's theorem#
For antitone w, a tuple x lies in the convex hull of the permutation
orbit of w exactly when x is majorized by w: the prefix sums of the decreasing
rearrangement of x are at most those of w, and the total sums agree.
TauCeti.mem_convexHull_range_comp_perm_iff {n : ℕ} {w x : Fin n → ℝ} (hw : Antitone w) :
x ∈ (convexHull ℝ) (Set.range fun σ => w ∘ ⇑σ) ↔
(∀ (k : ℕ), TauCeti.prefixSum k (x ∘ ⇑(Tuple.sortDesc x)) ≤ TauCeti.prefixSum k w) ∧
∑ i, x i = ∑ i, w i
Lean
Formalized in Tau Ceti as TauCeti.mem_convexHull_range_comp_perm_iff.
Other forms
Rado's theorem for antitone tuples. Formalized in Tau Ceti as TauCeti.mem_convexHull_range_comp_perm_iff_of_antitone.
TauCeti.mem_convexHull_range_comp_perm_iff_of_antitone {n : ℕ} {w x : Fin n → ℝ} (hw : Antitone w)
(hx : Antitone x) :
x ∈ (convexHull ℝ) (Set.range fun σ => w ∘ ⇑σ) ↔
(∀ (k : ℕ), TauCeti.prefixSum k x ≤ TauCeti.prefixSum k w) ∧ ∑ i, x i = ∑ i, w i
Sources
TheoremThe Vitali covering lemma for sections#
There is a constant C, depending only on E
and μ, with the following property. Let u be convex on an open set Ω, with
λ μ ≤ MA_u ≤ Λ μ on Ω for the Monge–Ampère measure of u extended by ⊤ off Ω and
0 < λ, and write θ = 1 + C Λ / λ. Suppose that every section of height H centred at a point
of D, with any supporting slope, is bounded with closure inside Ω. Consider a family of
sections S i = S(c i, h i), i ∈ t, with centres c i ∈ Ω, supporting slopes ℓ i, positive
heights with 4 θ h i ≤ H, and S i ⊆ D. Then there is a countable subfamily s ⊆ t of pairwise
disjoint sections such that every S i with i ∈ t lies in S(c j, 2 θ² h j) for some
j ∈ s.
TauCeti.exists_countable_pairwiseDisjoint_convexSection.{u_1, u_2} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E]
[MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] :
∃ C,
∀ {ι : Type u_2} (Ω : Set E) [inst : DecidablePred fun x => x ∈ Ω] (u : E → ℝ) (D : Set E)
(H : ℝ) (lam Lam : NNReal) (t : Set ι) (c : ι → E) (ℓ : ι → E →ₗ[ℝ] ℝ) (h : ι → ℝ),
IsOpen Ω →
ConvexOn ℝ Ω u →
(∀ z ∈ D,
∀ (n : E →ₗ[ℝ] ℝ),
(∀ w ∈ Ω, u z + (n w - n z) ≤ u w) →
Bornology.IsBounded (TauCeti.convexSection Ω u z n H) ∧
closure (TauCeti.convexSection Ω u z n H) ⊆ Ω) →
0 < lam →
(↑lam • μ.restrict Ω ≤
TauCeti.mongeAmpereMeasure μ fun y => if y ∈ Ω then ↑(u y) else ⊤) →
(TauCeti.mongeAmpereMeasure μ fun y => if y ∈ Ω then ↑(u y) else ⊤) ≤
↑Lam • μ.restrict Ω →
(∀ i ∈ t, c i ∈ Ω) →
(∀ i ∈ t, ∀ w ∈ Ω, u (c i) + ((ℓ i) w - (ℓ i) (c i)) ≤ u w) →
(∀ i ∈ t, TauCeti.convexSection Ω u (c i) (ℓ i) (h i) ⊆ D) →
(∀ i ∈ t, 0 < h i) →
(∀ i ∈ t, 4 * (1 + ↑C * ↑Lam / ↑lam) * h i ≤ H) →
∃ s ⊆ t,
s.Countable ∧
(s.PairwiseDisjoint fun i =>
TauCeti.convexSection Ω u (c i) (ℓ i) (h i)) ∧
∀ i ∈ t,
∃ j ∈ s,
TauCeti.convexSection Ω u (c i) (ℓ i) (h i) ⊆
TauCeti.convexSection Ω u (c j) (ℓ j)
(2 * (1 + ↑C * ↑Lam / ↑lam) ^ 2 * h j)
Lean
Formalized in Tau Ceti as TauCeti.exists_countable_pairwiseDisjoint_convexSection.
Other forms
The Vitali covering lemma for sections, measure form. Formalized in Tau Ceti as TauCeti.exists_countable_pairwiseDisjoint_convexSection_measure_le.
TauCeti.exists_countable_pairwiseDisjoint_convexSection_measure_le.{u_1, u_2} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E]
[MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] :
∃ C A,
∀ {ι : Type u_2} (Ω : Set E) [inst : DecidablePred fun x => x ∈ Ω] (u : E → ℝ) (D : Set E)
(H : ℝ) (lam Lam : NNReal) (t : Set ι) (c : ι → E) (ℓ : ι → E →ₗ[ℝ] ℝ) (h : ι → ℝ),
IsOpen Ω →
ConvexOn ℝ Ω u →
(∀ z ∈ D,
∀ (n : E →ₗ[ℝ] ℝ),
(∀ w ∈ Ω, u z + (n w - n z) ≤ u w) →
Bornology.IsBounded (TauCeti.convexSection Ω u z n H) ∧
closure (TauCeti.convexSection Ω u z n H) ⊆ Ω) →
0 < lam →
(↑lam • μ.restrict Ω ≤
TauCeti.mongeAmpereMeasure μ fun y => if y ∈ Ω then ↑(u y) else ⊤) →
(TauCeti.mongeAmpereMeasure μ fun y => if y ∈ Ω then ↑(u y) else ⊤) ≤
↑Lam • μ.restrict Ω →
(∀ i ∈ t, c i ∈ Ω) →
(∀ i ∈ t, ∀ w ∈ Ω, u (c i) + ((ℓ i) w - (ℓ i) (c i)) ≤ u w) →
(∀ i ∈ t, TauCeti.convexSection Ω u (c i) (ℓ i) (h i) ⊆ D) →
(∀ i ∈ t, 0 < h i) →
(∀ i ∈ t, 4 * (1 + ↑C * ↑Lam / ↑lam) * h i ≤ H) →
(∀ i ∈ t, 2 * (1 + ↑C * ↑Lam / ↑lam) ^ 2 * h i ≤ H) →
∃ s ⊆ t,
s.Countable ∧
(s.PairwiseDisjoint fun i =>
TauCeti.convexSection Ω u (c i) (ℓ i) (h i)) ∧
μ (⋃ i ∈ t, TauCeti.convexSection Ω u (c i) (ℓ i) (h i)) ≤
↑(NNReal.sqrt
(A *
(2 * (1 + C * Lam / lam) ^ 2) ^
Module.finrank ℝ E *
Lam /
lam)) *
μ (⋃ j ∈ s, TauCeti.convexSection Ω u (c j) (ℓ j) (h j))
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.