On this page
Clipped profiles: a constrained scalar variational problem
Imports 1 library modules and 22 external
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability
Required by 1 files of the paper proofs
For a law mu on the line, symmetric with a finite second moment sigma2 = E X^2, reals c > -1 and C >= 1, and a profile q, let
V_c(q) = 2 E[X q(X)] - E[q(X)^2] - c (E q(X))^2.
A profile is admissible for C when it is measurable with t <= q <= C t for some t >= 0, and admissible almost everywhere when these bounds hold mu-almost everywhere. For a real a and t >= 0, the clipped profile
q_{a,t}(x) = min (max (x - a) t) (C t)
is admissible; with l = t + a and u = C t + a it is t + (x - l)_+ - (x - u)_+, and q_{a,t}(x) is the point of [t, C t] closest to x - a. m and s are the upper moments of variational.v.
Main results:
- clip_first_order: under the balance m(-l) = C m(u), the residual w(x) = x - a - q_{a,t}(x) has E[w (q - q_{a,t})] <= 0 for every admissible q; clip_residual_profile: E[w q_{a,t}] = 0.
- clip_optimal: if moreover a = c E q_{a,t} (a fixed point), q_{a,t} maximizes V_c over the admissible profiles. clip_objective_profile: V_c(q_{a,t}) = E[X q_{a,t}(X)]; clip_objective_radial: V_c(q_{a,t}) = E[q_{a,t}(X)^2] + c (E q_{a,t}(X))^2; clip_objectiveE: V_c(q_{a,t}) = J(l) - J(u), with J(w) = s(w) + w m(w).
- clip_energy_shiftE: s(-t - a) + s(C t + a) = E (X - a - q_{a,t}(X))^2, the mean squared distance from X - a to [t, C t].
- The dual form, with clip_dual mu c C b the function D(b) = sigma2 + c (1 + c) b^2 - inf_(t' >= 0) (s(-t' - c b) + s(C t' + c b)), under the balance and the fixed point: clip_dual_opt: D(E q_{a,t}) = V_c(q_{a,t}); clip_dual_le: D(b) <= V_c(q_{a,t}) for every b if c <= 0; clip_dual_ge: V_c(q_{a,t}) <= D(b) for every b if c >= 0; clip_dual_window: 0 <= E q_{a,t} and min(1, 1 + c)^2 (E q_{a,t})^2 <= sigma2.
- clip_objective_add: for bounded measurable q and h, V_c(q + h) is V_c(q) + 2 E[(X - c E q(X) - q(X)) h(X)] - E[h(X)^2] - c (E h(X))^2; clip_admissible_le: a profile admissible for C is admissible for every C' >= C.
- For every law mu and all reals c and C: two measurable profiles equal almost everywhere have the same objective (clip_objective_ae_eq). If t <= q <= C t mu-almost everywhere, the clipped profile min(max(q, t), C t) is admissible for C (clip_ae_admissible), equals q almost everywhere (clip_ae_eq) and has the objective of q (clip_ae_objective). So V_c takes the same values on the two classes (clip_objective_ae_set) and has the same supremum on them (clip_value_ae). clip_admissible_ae_integrable: if mu has a finite second moment, the three integrands of V_c are integrable on the almost-everywhere class.
- Tools: clip_profile_mean, E q_{a,t} = t + m(l) - m(u); clip_energy_shift_min, t minimizes t' |-> s(-t' - a) + s(C t' + a); clip_dual_profile, clip_dual_lower; clip_res_sqE, the expansion of E (X - a - f(X))^2 for a bounded measurable f; the integrability of bounded measurable functions and of their products with x.
clip_ | min (max (x - a) t) (C t) |
clip_ | q measurable, t <= q <= C t, some t >= 0 |
clip_ | q measurable, t <= q <= C t mu-a.e., some t >= 0 |
clip_ | 2 E[X q] - E[q^2] - c (E q)^2 |
clip_ | s(-t - a) + s(C t + a) |
clip_ | E X^2 + c (1 + c) b^2 - inf_(t >= 0) clip_energy_shift mu C (c b) t |
Main results
| Results | Statement |
|---|---|
For a law mu on the line, symmetric with a finite second moment, reals C >= 1, t >= 0 and a, the clipped profile q(x) = min (max (x - a) t) (C t) is admissible (measurable, with t' <= q <= C t' for some t' >= 0), equals t + (x - t - a)_+ - (x - C t - a)_+, is the point of [t, C t] closest to x - a, and has mean t + m(t + a) - m(C t + a); clip_objective mu c q = 2 E[X q(X)] - E[q(X)^2] - c (E q(X))^2. | |
Under the balance m(-(t + a)) = C m(C t + a), the residual w(x) = x - a - q(x) satisfies E[w (q' - q)] <= 0 for every admissible q' and E[w q] = 0; if moreover a = c E q(X) with c > -1, then q maximizes clip_objective mu c over the admissible profiles, and its value is E[X q(X)] = J(t + a) - J(C t + a), J(w) = s(w) + w m(w). | |
The shifted clipping energy s(-t - a) + s(C t + a) is the mean squared distance from X - a to [t, C t], and under the balance it is minimal over t' >= 0 at t. The dual D(b) = E X^2 + c (1 + c) b^2 - inf_(t' >= 0) (s(-t' - c b) + s(C t' + c b)) satisfies, under the balance and the fixed point: D(E q(X)) = clip_objective mu c q, D(b) <= clip_objective mu c q for every b if -1 < c <= 0, clip_objective mu c q <= D(b) for every b if c >= 0 (this direction for every clipped profile), and 0 <= E q(X) with min(1, 1 + c)^2 (E q(X))^2 <= E X^2. | |
For bounded measurable q and h, clip_objective mu c (q + h) = clip_objective mu c q + 2 E[(X - c E q(X) - q(X)) h(X)] - E[h(X)^2] - c (E h(X))^2; under the balance and the fixed point, the clipped profile q has clip_objective mu c q = E[q(X)^2] + c (E q(X))^2; a profile admissible for C is admissible for every C' >= C. | |
For every law mu on the line and all reals c and C: two measurable profiles equal mu-almost everywhere have the same clip_objective mu c. If q is measurable and t <= q <= C t holds mu-almost everywhere for some t >= 0 (clip_admissible_ae mu C q), then the clipped profile min(max(q, t), C t) is admissible for C, equals q almost everywhere and has the objective of q. So clip_objective mu c takes the same values on the admissible profiles and on those admissible almost everywhere, and has the same supremum on the two classes. If mu has a finite second moment, then q, x q(x) and q(x)^2 are integrable for every q admissible almost everywhere. |
Declarations54 exported, 8 local
sectionclip_profile_def
Context {R : realType}.
Type
forall {R : realType}, R -> R -> R -> R -> RDefinition
Definition clip_profile (C a t : R) (x : R) : R := Num.min (Num.max (x - a) t) (C * t).
The clipped profile x |-> min (max (x - a) t) (C t).
Main result, as the README states it
For a law mu on the line, symmetric with a finite second moment, reals C >= 1, t >= 0 and a, the clipped profile q(x) = min (max (x - a) t) (C t) is admissible (measurable, with t' <= q <= C t' for some t' >= 0), equals t + (x - t - a)_+ - (x - C t - a)_+, is the point of [t, C t] closest to x - a, and has mean t + m(t + a) - m(C t + a); clip_objective mu c q = 2 E[X q(X)] - E[q(X)^2] - c (E q(X))^2.
Used by 22 declarations in 1 file
- this file: clip_profile_bounds, clip_profileE, clip_residualE, measurable_clip_profile, clip_profile_admissible, clip_profile_bounded, clip_profile_mean, clip_profile_closest, clip_energy_shiftE, clip_dual_profile, clip_first_order, clip_residual_profile, clip_objective_profile, clip_objective_radial, clip_optimal, clip_objectiveE, clip_energy_shift_min, clip_dual_lower, clip_dual_opt, clip_dual_le, clip_dual_ge, clip_dual_window
Type
forall {R : realType}, R -> set (measurableTypeR R -> R)
Definition
Definition clip_admissible (C : R) : set (measurableTypeR R -> R) := [set q | measurable_fun [set: measurableTypeR R] q /\ exists2 t : R, 0 <= t & forall x, t <= q x <= C * t].
The admissible profiles: measurable, with t <= q <= C t for some t >= 0.
Main result
Stated in the README together with clip_profile.
Used by 9 declarations in 1 file
forall {R : realType} [C C' : R] [q : measurableTypeR R -> R], C <= C' -> clip_admissible C q -> clip_admissible C' q
A profile admissible for C is admissible for every C' >= C.
Main result
Stated in the README together with clip_objective_add.
Statement as written in the source
Lemma clip_admissible_le (C C' : R) (q : measurableTypeR R -> R) : C <= C' -> clip_admissible C q -> clip_admissible C' q.
sectionclip_objective_def
Context {R : realType} (mu : probability (measurableTypeR R) R).
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> (measurableTypeR R -> R) -> R
Definition
Definition clip_objective (c : R) (q : measurableTypeR R -> R) : R := 2 * \int[mu]_x ((x : R) * q x) - \int[mu]_x (q x ^+ 2) - c * (\int[mu]_x q x) ^+ 2.
V_c(q) = 2 E[X q(X)] - E[q(X)^2] - c (E q(X))^2.
Main result
Stated in the README together with clip_profile.
Used by 15 declarations in 1 file
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> set (measurableTypeR R -> R)
Definition
Definition clip_admissible_ae (C : R) : set (measurableTypeR R -> R) := [set q | measurable_fun [set: measurableTypeR R] q /\ exists2 t : R, 0 <= t & {ae mu, forall x, t <= q x <= C * t}].
The profiles admissible for C almost everywhere: measurable, with t <= q <= C t mu-almost everywhere for some t >= 0.
Main result, as the README states it
For every law mu on the line and all reals c and C: two measurable profiles equal mu-almost everywhere have the same clip_objective mu c. If q is measurable and t <= q <= C t holds mu-almost everywhere for some t >= 0 (clip_admissible_ae mu C q), then the clipped profile min(max(q, t), C t) is admissible for C, equals q almost everywhere and has the objective of q. So clip_objective mu c takes the same values on the admissible profiles and on those admissible almost everywhere, and has the same supremum on the two classes. If mu has a finite second moment, then q, x q(x) and q(x)^2 are integrable for every q admissible almost everywhere.
Used by 4 declarations in 1 file
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> R -> R -> RDefinition
Definition clip_energy_shift (C a t : R) : R := upper_moment mu 2 (- t - a) + upper_moment mu 2 (C * t + a).
s(-t - a) + s(C t + a), the mean squared distance from X - a to [t, C t] for a symmetric law.
Main result, as the README states it
The shifted clipping energy s(-t - a) + s(C t + a) is the mean squared distance from X - a to [t, C t], and under the balance it is minimal over t' >= 0 at t. The dual D(b) = E X^2 + c (1 + c) b^2 - inf_(t' >= 0) (s(-t' - c b) + s(C t' + c b)) satisfies, under the balance and the fixed point: D(E q(X)) = clip_objective mu c q, D(b) <= clip_objective mu c q for every b if -1 < c <= 0, clip_objective mu c q <= D(b) for every b if c >= 0 (this direction for every clipped profile), and 0 <= E q(X) with min(1, 1 + c)^2 (E q(X))^2 <= E X^2.
Used by 10 declarations in 1 file
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> R -> R -> RDefinition
Definition clip_dual (c C b : R) : R := \int[mu]_x ((x : R) ^+ 2) + c * (1 + c) * b ^+ 2 - inf [set clip_energy_shift C (c * b) t | t in [set t : R | 0 <= t]].
D(b) = E X^2 + c (1 + c) b^2 - inf_(t >= 0) (s(-t - c b) + s(C t + c b)).
Main result
Stated in the README together with clip_energy_shift.
Used by 3 declarations in 1 file
- this file: clip_dual_opt, clip_dual_le, clip_dual_ge
sectionclip_profile_facts
Context {R : realType}. Variables (C a t : R). Hypotheses (C1 : 1 <= C) (t0 : 0 <= t). Local Notation q := (clip_profile C a t).
forall {R : realType} [C t : R], 1 <= C -> 0 <= t -> t <= C * tStatement as written in the source
Lemma clip_profile_ct : t <= C * t.
Used by 7 declarations in 1 file
forall {R : realType} [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> forall x : R, t <= clip_profile C a t x <= C * t
Statement as written in the source
Lemma clip_profile_bounds x : t <= q x <= C * t.
Used by 3 declarations in 1 file
- this file: clip_profile_admissible, clip_dual_lower, clip_dual_window
forall {R : realType} [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> forall x : R, clip_profile C a t x = t + maxr (x - (t + a)) 0 - maxr (x - (C * t + a)) 0
q(x) = t + (x - (t + a))_+ - (x - (C t + a))_+.
Main result
Stated in the README together with clip_profile.
Statement as written in the source
Lemma clip_profileE x : q x = t + Num.max (x - (t + a)) 0 - Num.max (x - (C * t + a)) 0.
Used by 5 declarations in 1 file
forall {R : realType} [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> forall x : R, x - a - clip_profile C a t x = maxr (x - (C * t + a)) 0 - maxr (t + a - x) 0
The residual x - a - q(x) is (x - u)_+ - (ell - x)_+.
Statement as written in the source
Lemma clip_residualE x : x - a - q x = Num.max (x - (C * t + a)) 0 - Num.max ((t + a) - x) 0.
Used by 3 declarations in 1 file
- this file: clip_energy_shiftE, clip_first_order, clip_residual_profile
forall {R : realType} (C a t : R), measurable_fun [set: measurableTypeR R] [eta clip_profile C a t]
Statement as written in the source
Lemma measurable_clip_profile : measurable_fun [set: measurableTypeR R] (fun x : measurableTypeR R => q x).
Used by 8 declarations in 1 file
forall {R : realType} [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> clip_admissible C [eta clip_profile C a t]
Statement as written in the source
Lemma clip_profile_admissible : clip_admissible C (fun x : measurableTypeR R => q x).
Used by 3 declarations in 1 file
- this file: clip_profile_bounded, clip_energy_shift_min, clip_dual_le
sectionclip_integrals
Context {R : realType} (mu : probability (measurableTypeR R) R). Hypothesis mu2 : mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)). Hypothesis musym : forall A : set (measurableTypeR R), measurable A -> mu ((fun x => - x) @^-1` A) = mu A. Local Notation m := (upper_moment mu 1). Local Notation s := (upper_moment mu 2). Local Notation integrable f := (mu.-integrable [set: measurableTypeR R] (EFin \o f)).
Let integrableZ_R (k : R) (f : measurableTypeR R -> R) : integrable f -> integrable (fun x => k * f x).
Used by 10 declarations in 1 file
Let integrableB_R (f g : measurableTypeR R -> R) : integrable f -> integrable g -> integrable (fun x => f x - g x).
Used by 6 declarations in 1 file
Let integrableD_R (f g : measurableTypeR R -> R) : integrable f -> integrable g -> integrable (fun x => f x + g x).
Used by 6 declarations in 1 file
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall [f : measurableTypeR R -> R] [B : R], measurable_fun [set: measurableTypeR R] f -> (forall x : measurableTypeR R, `|f x| <= B) -> mu.-integrable [set: measurableTypeR R] (EFin \o f)
Bounded measurable functions are integrable, and so is their product with the identity.
Statement as written in the source
Lemma clip_integrable_bounded (f : measurableTypeR R -> R) (B : R) : measurable_fun [set: measurableTypeR R] f -> (forall x, `|f x| <= B) -> integrable f.
Used by 11 declarations in 1 file
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall [f : measurableTypeR R -> R] [B : R], measurable_fun [set: measurableTypeR R] f -> (forall x : measurableTypeR R, `|f x| <= B) -> mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) * f x))
Statement as written in the source
Lemma clip_integrable_id_bounded (f : measurableTypeR R -> R) (B : R) : measurable_fun [set: measurableTypeR R] f -> (forall x, `|f x| <= B) -> integrable (fun x => (x : R) * f x).
Used by 6 declarations in 1 file
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall w : R, \int[mu]_x maxr (w - (x : R)) 0 = upper_moment mu 1 (- w)
E (w - X)_+ = m(-w) for a symmetric law.
Statement as written in the source
Lemma upper_moment1_reflect w : \int[mu]_x Num.max (w - (x : R)) 0 = m (- w).
Used by 2 declarations in 1 file
- this file: clip_first_order, clip_residual_profile
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall w : R, mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => maxr ((x : R) - w) 0))
Statement as written in the source
Lemma integrable_upper1 w : integrable (fun x => Num.max ((x : R) - w) 0).
Used by 6 declarations in 1 file
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall w : R, mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => maxr (w - (x : R)) 0))
Statement as written in the source
Lemma integrable_upper1_reflect w : integrable (fun x => Num.max (w - (x : R)) 0).
Used by 2 declarations in 1 file
- this file: clip_first_order, clip_residual_profile
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall [f : measurableTypeR R -> R] [B : R], measurable_fun [set: measurableTypeR R] f -> (forall x : measurableTypeR R, `|f x| <= B) -> mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x ^+ 2))
Statement as written in the source
Lemma clip_integrable_sq (f : measurableTypeR R -> R) (B : R) : measurable_fun [set: measurableTypeR R] f -> (forall x, `|f x| <= B) -> integrable (fun x => f x ^+ 2).
Used by 4 declarations in 1 file
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall [f g : measurableTypeR R -> R] [B B' : R], measurable_fun [set: measurableTypeR R] f -> measurable_fun [set: measurableTypeR R] g -> (forall x : measurableTypeR R, `|f x| <= B) -> (forall x : measurableTypeR R, `|g x| <= B') -> mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x * g x))
Statement as written in the source
Lemma clip_integrable_mul (f g : measurableTypeR R -> R) (B B' : R) : measurable_fun [set: measurableTypeR R] f -> measurable_fun [set: measurableTypeR R] g -> (forall x, `|f x| <= B) -> (forall x, `|g x| <= B') -> integrable (fun x => f x * g x).
Used by 1 declaration in 1 file
- this file: clip_objective_add
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall (a : R) [f g : measurableTypeR R -> R] [B B' : R], measurable_fun [set: measurableTypeR R] f -> measurable_fun [set: measurableTypeR R] g -> (forall x : measurableTypeR R, `|f x| <= B) -> (forall x : measurableTypeR R, `|g x| <= B') -> mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => ((x : R) - a - f x) * g x))
The residual x - a - f(x) of a bounded measurable f, times a bounded measurable g, and squared.
Statement as written in the source
Lemma clip_integrable_res_mul (a : R) (f g : measurableTypeR R -> R) (B B' : R) : measurable_fun [set: measurableTypeR R] f -> measurable_fun [set: measurableTypeR R] g -> (forall x, `|f x| <= B) -> (forall x, `|g x| <= B') -> integrable (fun x => ((x : R) - a - f x) * g x).
Used by 1 declaration in 1 file
- this file: clip_energy_shift_min
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall (a : R) [f : measurableTypeR R -> R] [B : R], measurable_fun [set: measurableTypeR R] f -> (forall x : measurableTypeR R, `|f x| <= B) -> mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => ((x : R) - a - f x) ^+ 2))
Statement as written in the source
Lemma clip_integrable_res_sq (a : R) (f : measurableTypeR R -> R) (B : R) : measurable_fun [set: measurableTypeR R] f -> (forall x, `|f x| <= B) -> integrable (fun x => ((x : R) - a - f x) ^+ 2).
Used by 2 declarations in 1 file
- this file: clip_energy_shift_min, clip_dual_lower
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall (a : R) [f : measurableTypeR R -> R] [B : R], measurable_fun [set: measurableTypeR R] f -> (forall x : measurableTypeR R, `|f x| <= B) -> \int[mu]_x ((x : R) - a - f x) ^+ 2 = \int[mu]_x (x : R) ^+ 2 + a ^+ 2 - 2 * \int[mu]_x ((x : R) * f x) + 2 * a * \int[mu]_x f x + \int[mu]_x f x ^+ 2
E (X - a - f(X))^2, expanded, for a bounded measurable f.
Statement as written in the source
Lemma clip_res_sqE (a : R) (f : measurableTypeR R -> R) (B : R) : measurable_fun [set: measurableTypeR R] f -> (forall x, `|f x| <= B) -> \int[mu]_x (((x : R) - a - f x) ^+ 2) = \int[mu]_x ((x : R) ^+ 2) + a ^+ 2 - 2 * \int[mu]_x ((x : R) * f x) + 2 * a * \int[mu]_x f x + \int[mu]_x (f x ^+ 2).
Used by 3 declarations in 1 file
- this file: clip_dual_profile, clip_dual_lower, clip_dual_window
forall {R : realType} [C : R] [q' : measurableTypeR R -> R], clip_admissible C q' -> exists2 B : R, 0 <= B & forall x : measurableTypeR R, `|q' x| <= B
Statement as written in the source
Lemma clip_admissible_bounded (C : R) (q' : measurableTypeR R -> R) : clip_admissible C q' -> exists2 B : R, 0 <= B & forall x, `|q' x| <= B.
Used by 4 declarations in 1 file
forall {R : realType} [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> exists2 B : R, 0 <= B & forall x : R, `|clip_profile C a t x| <= B
Statement as written in the source
Lemma clip_profile_bounded (C a t : R) : 1 <= C -> 0 <= t -> exists2 B : R, 0 <= B & forall x, `|clip_profile C a t x| <= B.
Used by 8 declarations in 1 file
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> \int[mu]_x clip_profile C a t x = t + upper_moment mu 1 (t + a) - upper_moment mu 1 (C * t + a)
E q_{a,t} = t + m(t + a) - m(C t + a).
Main result
Stated in the README together with clip_profile.
Statement as written in the source
Lemma clip_profile_mean (C a t : R) : 1 <= C -> 0 <= t -> \int[mu]_x clip_profile C a t x = t + m (t + a) - m (C * t + a).
forall {R : realType} [C : R] (a : R) [t : R] (x : R) [z : R], 1 <= C -> 0 <= t -> t <= z <= C * t -> (x - a - clip_profile C a t x) ^+ 2 <= (x - a - z) ^+ 2
q_{a,t}(x) is the point of [t, C t] closest to x - a.
Main result
Stated in the README together with clip_profile.
Statement as written in the source
Lemma clip_profile_closest (C a t : R) (x z : R) : 1 <= C -> 0 <= t -> t <= z <= C * t -> (x - a - clip_profile C a t x) ^+ 2 <= (x - a - z) ^+ 2.
Used by 1 declaration in 1 file
- this file: clip_dual_lower
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> clip_energy_shift mu C a t = \int[mu]_x ((x : R) - a - clip_profile C a t x) ^+ 2
s(-t - a) + s(C t + a) = E (X - a - q_{a,t}(X))^2.
Main result
Stated in the README together with clip_energy_shift.
Statement as written in the source
Lemma clip_energy_shiftE (C a t : R) : 1 <= C -> 0 <= t -> clip_energy_shift mu C a t = \int[mu]_x (((x : R) - a - clip_profile C a t x) ^+ 2).
Used by 3 declarations in 1 file
- this file: clip_dual_profile, clip_energy_shift_min, clip_dual_lower
forall {R : realType} (mu : probability (measurableTypeR R) R) (C a t : R), 0 <= clip_energy_shift mu C a t
Statement as written in the source
Lemma clip_energy_shift_ge0 (C a t : R) : 0 <= clip_energy_shift mu C a t.
Used by 1 declaration in 1 file
- this file: S_lbound
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall (c : R) [C : R] (b : R) [t : R], 1 <= C -> 0 <= t -> \int[mu]_x (x : R) ^+ 2 + c * (1 + c) * b ^+ 2 - clip_energy_shift mu C (c * b) t = clip_objective mu c (clip_profile C (c * b) t) + c * (\int[mu]_x clip_profile C (c * b) t x - b) ^+ 2
D(b) without the infimum, at a clipped profile: E X^2 + c (1 + c) b^2 - (s(-t - c b) + s(C t + c b)) = V_c(q_{c b, t}) + c (E q_{c b, t} - b)^2.
Main result
Stated in the README together with clip_energy_shift.
Statement as written in the source
Lemma clip_dual_profile (c C b t : R) : 1 <= C -> 0 <= t -> \int[mu]_x ((x : R) ^+ 2) + c * (1 + c) * b ^+ 2 - clip_energy_shift mu C (c * b) t = clip_objective mu c (clip_profile C (c * b) t) + c * (\int[mu]_x clip_profile C (c * b) t x - b) ^+ 2.
Used by 2 declarations in 1 file
- this file: clip_dual_opt, clip_dual_le
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall (c : R) [q h : measurableTypeR R -> R] [B B' : R], measurable_fun [set: measurableTypeR R] q -> measurable_fun [set: measurableTypeR R] h -> (forall x : measurableTypeR R, `|q x| <= B) -> (forall x : measurableTypeR R, `|h x| <= B') -> clip_objective mu c (fun x : measurableTypeR R => q x + h x) = clip_objective mu c q + 2 * \int[mu]_x (((x : R) - c * \int[mu]_y q y - q x) * h x) - (\int[mu]_x h x ^+ 2 + c * (\int[mu]_x h x) ^+ 2)
The expansion of V_c around a bounded measurable q, in a bounded measurable direction h: V_c(q + h) = V_c(q) + 2 E[(X - c E q - q(X)) h(X)] - (E h^2 + c (E h)^2).
Main result, as the README states it
For bounded measurable q and h, clip_objective mu c (q + h) = clip_objective mu c q + 2 E[(X - c E q(X) - q(X)) h(X)] - E[h(X)^2] - c (E h(X))^2; under the balance and the fixed point, the clipped profile q has clip_objective mu c q = E[q(X)^2] + c (E q(X))^2; a profile admissible for C is admissible for every C' >= C.
Statement as written in the source
Lemma clip_objective_add (c : R) (q h : measurableTypeR R -> R) (B B' : R) : measurable_fun [set: measurableTypeR R] q -> measurable_fun [set: measurableTypeR R] h -> (forall x, `|q x| <= B) -> (forall x, `|h x| <= B') -> clip_objective mu c (fun x => q x + h x) = clip_objective mu c q + 2 * \int[mu]_x (((x : R) - c * \int[mu]_y q y - q x) * h x) - (\int[mu]_x (h x ^+ 2) + c * (\int[mu]_x h x) ^+ 2).
- The first-order inequality under the balance m(-ell) = C m(u).
sectionclip_first_order
Variables (C a t : R). Hypotheses (C1 : 1 <= C) (t0 : 0 <= t). Hypothesis balance : m (- (t + a)) = C * m (C * t + a). Local Notation q := (clip_profile C a t).
Let C0 : 0 <= C := le_trans ler01 C1.
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [q' : measurableTypeR R -> R], clip_admissible C q' -> \int[mu]_x ((x - a - clip_profile C a t x) * (q' x - clip_profile C a t x)) <= 0
E[w (q' - q)] <= 0 for every admissible q', w(x) = x - a - q(x).
Main result, as the README states it
Under the balance m(-(t + a)) = C m(C t + a), the residual w(x) = x - a - q(x) satisfies E[w (q' - q)] <= 0 for every admissible q' and E[w q] = 0; if moreover a = c E q(X) with c > -1, then q maximizes clip_objective mu c over the admissible profiles, and its value is E[X q(X)] = J(t + a) - J(C t + a), J(w) = s(w) + w m(w).
Statement as written in the source
Lemma clip_first_order (q' : measurableTypeR R -> R) : clip_admissible C q' -> \int[mu]_x ((x - a - q x) * (q' x - q x)) <= 0.
Used by 2 declarations in 1 file
- this file: clip_optimal, clip_energy_shift_min
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> \int[mu]_x ((x - a - clip_profile C a t x) * clip_profile C a t x) = 0
E[w q] = 0.
Main result
Stated in the README together with clip_first_order.
Statement as written in the source
Lemma clip_residual_profile : \int[mu]_x ((x - a - q x) * q x) = 0.
Used by 1 declaration in 1 file
- this file: clip_objective_profile
- Optimality and value, under the fixed point a = c E q.
Variable c : R. Hypothesis c1 : -1 < c. Hypothesis fixpt : a = c * \int[mu]_x q x.
Let bounded_sq (f : measurableTypeR R -> R) (B : R) : measurable_fun [set: measurableTypeR R] f -> (forall x, `|f x| <= B) -> integrable (fun x => f x ^+ 2).
Used by 2 declarations in 1 file
- this file: clip_objective_profile, clip_optimal
Let bounded_mul (f g : measurableTypeR R -> R) (B B' : R) : measurable_fun [set: measurableTypeR R] f -> measurable_fun [set: measurableTypeR R] g -> (forall x, `|f x| <= B) -> (forall x, `|g x| <= B') -> integrable (fun x => f x * g x).
Used by 1 declaration in 1 file
- this file: clip_optimal
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [c : R], a = c * \int[mu]_x clip_profile C a t x -> clip_objective mu c (clip_profile C a t) = \int[mu]_x ((x : R) * clip_profile C a t x)
E[X q] = E[q^2] + c (E q)^2, so V_c(q) = E[X q].
Main result
Stated in the README together with clip_first_order.
Statement as written in the source
Lemma clip_objective_profile : clip_objective mu c q = \int[mu]_x ((x : R) * q x).
Used by 3 declarations in 1 file
- this file: clip_objective_radial, clip_objectiveE, clip_dual_window
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [c : R], a = c * \int[mu]_x clip_profile C a t x -> clip_objective mu c (clip_profile C a t) = \int[mu]_x clip_profile C a t x ^+ 2 + c * (\int[mu]_x clip_profile C a t x) ^+ 2
The radial identity V_c(q) = E q^2 + c (E q)^2.
Main result
Stated in the README together with clip_objective_add.
Statement as written in the source
Lemma clip_objective_radial : clip_objective mu c q = \int[mu]_x (q x ^+ 2) + c * (\int[mu]_x q x) ^+ 2.
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [c : R], -1 < c -> a = c * \int[mu]_x clip_profile C a t x -> forall [q' : measurableTypeR R -> R], clip_admissible C q' -> clip_objective mu c q' <= clip_objective mu c (clip_profile C a t)
q maximizes V_c over the admissible profiles.
Main result
Stated in the README together with clip_first_order.
Statement as written in the source
Lemma clip_optimal (q' : measurableTypeR R -> R) : clip_admissible C q' -> clip_objective mu c q' <= clip_objective mu c q.
Used by 1 declaration in 1 file
- this file: clip_dual_le
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall w : R, mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) * maxr ((x : R) - w) 0))
E[X (X - w)_+] = s(w) + w m(w).
Statement as written in the source
Lemma clip_xupper_integrable w : integrable (fun x => (x : R) * Num.max ((x : R) - w) 0).
Used by 1 declaration in 1 file
- this file: clip_objectiveE
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> forall w : R, \int[mu]_x ((x : R) * maxr ((x : R) - w) 0) = upper_moment mu 2 w + w * upper_moment mu 1 w
Statement as written in the source
Lemma clip_xupperE w : \int[mu]_x ((x : R) * Num.max ((x : R) - w) 0) = s w + w * m w.
Used by 1 declaration in 1 file
- this file: clip_objectiveE
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [c : R], a = c * \int[mu]_x clip_profile C a t x -> clip_objective mu c (clip_profile C a t) = upper_moment mu 2 (t + a) + (t + a) * upper_moment mu 1 (t + a) - (upper_moment mu 2 (C * t + a) + (C * t + a) * upper_moment mu 1 (C * t + a))
V_c(q) = J(t + a) - J(C t + a), with J(w) = s(w) + w m(w).
Main result
Stated in the README together with clip_first_order.
Statement as written in the source
Lemma clip_objectiveE : clip_objective mu c q = (s (t + a) + (t + a) * m (t + a)) - (s (C * t + a) + (C * t + a) * m (C * t + a)).
- The dual form.
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [t' : R], 0 <= t' -> clip_energy_shift mu C a t <= clip_energy_shift mu C a t'
t minimizes t' |-> s(-t' - a) + s(C t' + a) over t' >= 0.
Main result
Stated in the README together with clip_energy_shift.
Statement as written in the source
Lemma clip_energy_shift_min (t' : R) : 0 <= t' -> clip_energy_shift mu C a t <= clip_energy_shift mu C a t'.
Used by 1 declaration in 1 file
- this file: clip_dual_opt
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> forall c b : R, clip_objective mu c (clip_profile C a t) + c * (b - \int[mu]_x clip_profile C a t x) ^+ 2 <= \int[mu]_x (x : R) ^+ 2 + c * (1 + c) * b ^+ 2 - clip_energy_shift mu C (c * b) t
V_c(q) + c (b - E q)^2 <= E X^2 + c (1 + c) b^2 - (s(-t - c b) + s(C t + c b)).
Statement as written in the source
Lemma clip_dual_lower (b : R) : clip_objective mu c q + c * (b - \int[mu]_x q x) ^+ 2 <= \int[mu]_x ((x : R) ^+ 2) + c * (1 + c) * b ^+ 2 - clip_energy_shift mu C (c * b) t.
Used by 1 declaration in 1 file
- this file: clip_dual_ge
Let S_lbound (a' : R) : has_lbound [set clip_energy_shift mu C a' t' | t' in [set t' : R | 0 <= t']].
Used by 2 declarations in 1 file
- this file: clip_dual_opt, clip_dual_ge
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [c : R], a = c * \int[mu]_x clip_profile C a t x -> clip_dual mu c C (\int[mu]_x clip_profile C a t x) = clip_objective mu c (clip_profile C a t)
The dual at its optimum: D(E q) = V_c(q); the infimum is attained at t.
Main result
Stated in the README together with clip_energy_shift.
Statement as written in the source
Lemma clip_dual_opt : clip_dual mu c C (\int[mu]_x q x) = clip_objective mu c q.
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [c : R], -1 < c -> a = c * \int[mu]_x clip_profile C a t x -> c <= 0 -> forall b : R, clip_dual mu c C b <= clip_objective mu c (clip_profile C a t)
For c <= 0, D(b) <= V_c(q) for every b.
Main result
Stated in the README together with clip_energy_shift.
Statement as written in the source
Lemma clip_dual_le : c <= 0 -> forall b, clip_dual mu c C b <= clip_objective mu c q.
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C : R] (a : R) [t : R], 1 <= C -> 0 <= t -> forall [c : R], 0 <= c -> forall b : R, clip_objective mu c (clip_profile C a t) <= clip_dual mu c C b
For c >= 0, V_c(q) <= D(b) for every b.
Main result
Stated in the README together with clip_energy_shift.
Statement as written in the source
Lemma clip_dual_ge : 0 <= c -> forall b, clip_objective mu c q <= clip_dual mu c C b.
forall {R : realType} [mu : probability (measurableTypeR R) R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> (forall A : set (measurableTypeR R), (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) -> forall [C a t : R], 1 <= C -> 0 <= t -> upper_moment mu 1 (- (t + a)) = C * upper_moment mu 1 (C * t + a) -> forall [c : R], -1 < c -> a = c * \int[mu]_x clip_profile C a t x -> 0 <= \int[mu]_x clip_profile C a t x /\ minr 1 (1 + c) ^+ 2 * (\int[mu]_x clip_profile C a t x) ^+ 2 <= \int[mu]_x (x : R) ^+ 2
The window: 0 <= E q and min(1, 1 + c)^2 (E q)^2 <= E X^2.
Main result
Stated in the README together with clip_energy_shift.
Statement as written in the source
Lemma clip_dual_window : 0 <= \int[mu]_x q x /\ Num.min 1 (1 + c) ^+ 2 * (\int[mu]_x q x) ^+ 2 <= \int[mu]_x ((x : R) ^+ 2).
sectionclip_ae
Context {R : realType} (mu : probability (measurableTypeR R) R). Local Notation integrable f := (mu.-integrable [set: measurableTypeR R] (EFin \o f)).
forall {R : realType} (mu : probability (measurableTypeR R) R) [C : R], clip_admissible C `<=` clip_admissible_ae mu C
An admissible profile is admissible almost everywhere.
Statement as written in the source
Lemma clip_admissible_ae_sub (C : R) : clip_admissible C `<=` clip_admissible_ae mu C.
Used by 1 declaration in 1 file
- this file: clip_objective_ae_set
forall {R : realType} [mu : probability (measurableTypeR R) R] [C t : R] [q : measurableTypeR R -> R], (\forall x \ae mu, t <= q x <= C * t) -> t <= C * t
If t <= q <= C t almost everywhere, then t <= C t, since mu is a probability.
Statement as written in the source
Lemma clip_ae_le (C t : R) (q : measurableTypeR R -> R) : {ae mu, forall x, t <= q x <= C * t} -> t <= C * t.
Used by 1 declaration in 1 file
- this file: clip_ae_admissible
forall {R : realType} [mu : probability (measurableTypeR R) R] (c : R) [q q' : measurableTypeR R -> R], measurable_fun [set: measurableTypeR R] q -> measurable_fun [set: measurableTypeR R] q' -> (\forall x \ae mu, q x = q' x) -> clip_objective mu c q = clip_objective mu c q'
Two measurable profiles equal almost everywhere have the same objective.
Main result
Stated in the README together with clip_admissible_ae.
Statement as written in the source
Lemma clip_objective_ae_eq (c : R) (q q' : measurableTypeR R -> R) : measurable_fun [set: measurableTypeR R] q -> measurable_fun [set: measurableTypeR R] q' -> {ae mu, forall x, q x = q' x} -> clip_objective mu c q = clip_objective mu c q'.
Used by 1 declaration in 1 file
- this file: clip_ae_objective
Let integrable_ae_eq (f g : measurableTypeR R -> R) : measurable_fun [set: measurableTypeR R] f -> {ae mu, forall x, f x = g x} -> integrable g -> integrable f.
A measurable function equal almost everywhere to an integrable one is integrable.
Used by 1 declaration in 1 file
- this file: clip_admissible_ae_integrable
sectionclip_ae_profile
Variables (C t : R) (q : measurableTypeR R -> R). Hypotheses (mq : measurable_fun [set: measurableTypeR R] q) (t0 : 0 <= t). Hypothesis hq : {ae mu, forall x, t <= q x <= C * t}.
forall {R : realType} [mu : probability (measurableTypeR R) R] [C t : R] [q : measurableTypeR R -> R], measurable_fun [set: measurableTypeR R] q -> 0 <= t -> (\forall x \ae mu, t <= q x <= C * t) -> clip_admissible C (fun x : measurableTypeR R => minr (maxr (q x) t) (C * t))
The clipped profile min(max(q, t), C t) is admissible for C.
Main result
Stated in the README together with clip_admissible_ae.
Statement as written in the source
Lemma clip_ae_admissible : clip_admissible C (fun x => Num.min (Num.max (q x) t) (C * t)).
Used by 3 declarations in 1 file
forall {R : realType} [mu : probability (measurableTypeR R) R] [C t : R] [q : measurableTypeR R -> R], (\forall x \ae mu, t <= q x <= C * t) -> \forall x \ae mu, minr (maxr (q x) t) (C * t) = q x
It equals q almost everywhere.
Main result
Stated in the README together with clip_admissible_ae.
Statement as written in the source
Lemma clip_ae_eq : {ae mu, forall x, Num.min (Num.max (q x) t) (C * t) = q x}.
Used by 2 declarations in 1 file
- this file: clip_ae_objective, clip_admissible_ae_integrable
forall {R : realType} [mu : probability (measurableTypeR R) R] [C t : R] [q : measurableTypeR R -> R], measurable_fun [set: measurableTypeR R] q -> 0 <= t -> (\forall x \ae mu, t <= q x <= C * t) -> forall c : R, clip_objective mu c (fun x : measurableTypeR R => minr (maxr (q x) t) (C * t)) = clip_objective mu c q
It has the objective of q.
Main result
Stated in the README together with clip_admissible_ae.
Statement as written in the source
Lemma clip_ae_objective (c : R) : clip_objective mu c (fun x => Num.min (Num.max (q x) t) (C * t)) = clip_objective mu c q.
Used by 1 declaration in 1 file
- this file: clip_objective_ae_set
forall {R : realType} (mu : probability (measurableTypeR R) R) (c C : R), [set clip_objective mu c q | q in clip_admissible_ae mu C] = [set clip_objective mu c q | q in clip_admissible C]
V_c takes the same values on the profiles admissible almost everywhere as on the admissible profiles, so the two problems have the same value.
Main result
Stated in the README together with clip_admissible_ae.
Statement as written in the source
Lemma clip_objective_ae_set (c C : R) : [set clip_objective mu c q | q in clip_admissible_ae mu C] = [set clip_objective mu c q | q in clip_admissible C].
Used by 1 declaration in 1 file
- this file: clip_value_ae
forall {R : realType} (mu : probability (measurableTypeR R) R) (c C : R), sup [set clip_objective mu c q | q in clip_admissible_ae mu C] = sup [set clip_objective mu c q | q in clip_admissible C]
Main result
Stated in the README together with clip_admissible_ae.
Statement as written in the source
Lemma clip_value_ae (c C : R) : sup [set clip_objective mu c q | q in clip_admissible_ae mu C] = sup [set clip_objective mu c q | q in clip_admissible C].
forall {R : realType} [mu : probability (measurableTypeR R) R] [C : R] [q : measurableTypeR R -> R], mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) -> clip_admissible_ae mu C q -> [/\ mu.-integrable [set: measurableTypeR R] (EFin \o q), mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) * q x)) & mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => q x ^+ 2))]
The three integrands of V_c are integrable at a profile admissible almost everywhere, when mu has a finite second moment.
Main result
Stated in the README together with clip_admissible_ae.
Statement as written in the source
Lemma clip_admissible_ae_integrable (C : R) (q : measurableTypeR R -> R) : mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)) -> clip_admissible_ae mu C q -> [/\ integrable q, integrable (fun x => (x : R) * q x) & integrable (fun x => q x ^+ 2)].