Imports
import Mathlib.Tactic import Analysis.Section_9_6 import Analysis.Section_11_3

Analysis I, Section 11.4: Basic properties of the Riemann integral

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Basic properties of the Riemann integral.

namespace Chapter11open Chapter9

Theorem 11.4.1(a) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.add {I: BoundedInterval} {f g: } (hf: IntegrableOn f I) (hg: IntegrableOn g I) : IntegrableOn (f + g) I integ (f + g) I = integ f I + integ g I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f + g) I integ (f + g) I = integ f I + integ g I All goals completed! 🐙

Theorem 11.4.1(b) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.smul {I: BoundedInterval} (c:) {f: } (hf: IntegrableOn f I) : IntegrableOn (c f) I integ (c f) I = c * integ f I := I:BoundedIntervalc:f: hf:IntegrableOn f IIntegrableOn (c f) I integ (c f) I = c * integ f I All goals completed! 🐙
theorem IntegrableOn.neg {I: BoundedInterval} {f: } (hf: IntegrableOn f I) : IntegrableOn (-f) I integ (-f) I = -integ f I := I:BoundedIntervalf: hf:IntegrableOn f IIntegrableOn (-f) I integ (-f) I = -integ f I I:BoundedIntervalf: hf:IntegrableOn f Ithis:IntegrableOn (-1 f) I integ (-1 f) I = -1 * integ f IIntegrableOn (-f) I integ (-f) I = -integ f I; All goals completed! 🐙

Theorem 11.4.1(c) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.sub {I: BoundedInterval} {f g: } (hf: IntegrableOn f I) (hg: IntegrableOn g I) : IntegrableOn (f - g) I integ (f - g) I = integ f I - integ g I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f - g) I integ (f - g) I = integ f I - integ g I All goals completed! 🐙

Theorem 11.4.1(d) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.nonneg {I: BoundedInterval} {f: } (hf: IntegrableOn f I) (hf_nonneg: x I, 0 f x) : 0 integ f I := I:BoundedIntervalf: hf:IntegrableOn f Ihf_nonneg: x I, 0 f x0 integ f I All goals completed! 🐙

Theorem 11.4.1(e) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.mono {I: BoundedInterval} {f g: } (hf: IntegrableOn f I) (hg: IntegrableOn g I) (h: MajorizesOn g f I) : integ f I integ g I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ih:MajorizesOn g f Iinteg f I integ g I All goals completed! 🐙

Theorem 11.4.1(f) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.const (c:) (I: BoundedInterval) : IntegrableOn (fun _ c) I integ (fun _ c) I = c * |I|ₗ := c:I:BoundedIntervalIntegrableOn (fun x c) I integ (fun x c) I = c * I.length All goals completed! 🐙

Theorem 11.4.1(f) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.const' {I: BoundedInterval} {f: } (hf: ConstantOn f I) : IntegrableOn f I integ f I = (constant_value_on f I) * |I|ₗ := I:BoundedIntervalf: hf:ConstantOn f IIntegrableOn f I integ f I = constant_value_on f I * I.length All goals completed! 🐙

Theorem 11.4.1 (g) / Exercise 11.4.1

open Classical intheorem declaration uses `sorry`IntegrableOn.of_extend {I J: BoundedInterval} (hIJ: I J) {f: } (h: IntegrableOn f I) : IntegrableOn (fun x if x I then f x else 0) J := I:BoundedIntervalJ:BoundedIntervalhIJ:I Jf: h:IntegrableOn f IIntegrableOn (fun x if x I then f x else 0) J All goals completed! 🐙

Theorem 11.4.1 (g) / Exercise 11.4.1

open Classical intheorem declaration uses `sorry`IntegrableOn.of_extend' {I J: BoundedInterval} (hIJ: I J) {f: } (h: IntegrableOn f I) : integ (fun x if x I then f x else 0) J = integ f I := I:BoundedIntervalJ:BoundedIntervalhIJ:I Jf: h:IntegrableOn f Iinteg (fun x if x I then f x else 0) J = integ f I All goals completed! 🐙

Theorem 11.4.1 (h) (Laws of integration) / Exercise 11.4.1

theorem declaration uses `sorry`IntegrableOn.join {I J K: BoundedInterval} (hIJK: K.joins I J) {f: } (h: IntegrableOn f K) : IntegrableOn f I IntegrableOn f J integ f K = integ f I + integ f J := I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalhIJK:K.joins I Jf: h:IntegrableOn f KIntegrableOn f I IntegrableOn f J integ f K = integ f I + integ f J All goals completed! 🐙

A variant of Theorem 11.4.1(h) that will be useful in later sections.

theorem declaration uses `sorry`IntegrableOn.mono' {I J: BoundedInterval} (hIJ: J I) {f: } (h: IntegrableOn f I) : IntegrableOn f J := I:BoundedIntervalJ:BoundedIntervalhIJ:J If: h:IntegrableOn f IIntegrableOn f J All goals completed! 🐙

A further variant of Theorem 11.4.1(h) that will be useful in later sections.

theorem declaration uses `sorry`IntegrableOn.eq {I J: BoundedInterval} (hIJ: J I) (ha: J.a = I.a) (hb: J.b = I.b) {f: } (h: IntegrableOn f I) : integ f J = integ f I := I:BoundedIntervalJ:BoundedIntervalhIJ:J Iha:J.a = I.ahb:J.b = I.bf: h:IntegrableOn f Iinteg f J = integ f I All goals completed! 🐙

A handy little lemma for "epsilon of room" type arguments

lemma nonneg_of_le_const_mul_eps {x C:} (h: ε>0, x C * ε) : x 0 := x:C:h: ε > 0, x C * εx 0 x:C:h: ε > 0, x C * εhC:C > 0x 0x:C:h: ε > 0, x C * εhC:¬C > 0x 0 x:C:h: ε > 0, x C * εhC:C > 0x 0 x:C:h: ε > 0, x C * εhC:C > 0this:0 < xFalse specialize h (x/(2*C)) (x:C:h: ε > 0, x C * εhC:C > 0this:0 < xx / (2 * C) > 0 All goals completed! 🐙); x:C:hC:C > 0this:0 < xh:x C * (x / (2 * C))C * (x / (2 * C)) = x / 2x:C:hC:C > 0this:0 < xh:x x / 2False; x:C:hC:C > 0this:0 < xh:x x / 2False All goals completed! 🐙 x:C:h: ε > 0, x C * εhC:¬C > 01 > 0x:C:hC:¬C > 0h:x C * 1x 0 x:C:h: ε > 0, x C * εhC:¬C > 01 > 0x:C:hC:¬C > 0h:x C * 1x 0 All goals completed! 🐙

Theorem 11.4.3 (Max and min preserve integrability)

theorem declaration uses `sorry`IntegrableOn.max {I: BoundedInterval} {f g: } (hf: IntegrableOn f I) (hg: IntegrableOn g I) : IntegrableOn (f g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I -- This proof is written to follow the structure of the original text. I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IIntegrableOn (f g) I have hmax_bound : BddOn (f g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IM:hM: x I, |f x| MBddOn (f g) I; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IM:hM: x I, |f x| MM':hM': x I, |g x| M'BddOn (f g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IM:hM: x I, |f x| MM':hM': x I, |g x| M' x I, |(f g) x| Max.max M M'; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IM:hM✝: x I, |f x| MM':hM': x I, |g x| M'x:hx:x IhM:|f x| M|(f g) x| Max.max M M'; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IM:hM✝: x I, |f x| MM':x:hx:x IhM:|f x| MhM':|g x| M'|(f g) x| Max.max M M' I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IM:hM✝: x I, |f x| MM':x:hx:x IhM:|f x| MhM':|g x| M'|Max.max (f x) (g x)| Max.max M M' All goals completed! 🐙 have lower_le_upper : 0 upper_integral (f g) I - lower_integral (f g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙 have (ε:) (: 0 < ε) : upper_integral (f g) I - lower_integral (f g) I 4*ε := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I choose f' hf'min hf'const hf'int using gt_of_lt_lower_integral hf.1 (show integ f I - ε < lower_integral f I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙) choose g' hg'min hg'const hg'int using gt_of_lt_lower_integral hg.1 (show integ g I - ε < lower_integral g I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙) choose f'' hf''max hf''const hf''int using lt_of_gt_upper_integral hf.1 (show upper_integral f I < integ f I + ε I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙) choose g'' hg''max hg''const hg''int using lt_of_gt_upper_integral hg.1 (show upper_integral g I < integ g I + ε I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Iupper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Iupper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Iupper_integral (f g) I - lower_integral (f g) I 4 * ε have hinteg_le : integ h I 4 * ε := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Iupper_integral (f g) I - lower_integral (f g) I 4 * ε have hf''g''_maj : MajorizesOn (f'' g'') (f g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Iupper_integral (f g) I - lower_integral (f g) I 4 * ε have hf'g'_maj : MinorizesOn (f' g') (f g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Iupper_integral (f g) I - lower_integral (f g) I 4 * ε have : MinorizesOn (f'' g'') (f' g' + h) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f x(f'' g'') x (f' g' + h) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g x(f'' g'') x (f' g' + h) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf''max:f x f'' x(f'' g'') x (f' g' + h) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf''max:f x f'' xhg''max:g x g'' x(f'' g'') x (f' g' + h) x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf''max:f x f'' xhg''max:g x g'' xf'' x Max.max (f' x) (g' x) + (f'' x - f' x + (g'' x - g' x)) g'' x Max.max (f' x) (g' x) + (f'' x - f' x + (g'' x - g' x)); I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf''max:f x f'' xhg''max:g x g'' xf'' x Max.max (f' x) (g' x) + (f'' x - f' x + (g'' x - g' x))I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf''max:f x f'' xhg''max:g x g'' xg'' x Max.max (f' x) (g' x) + (f'' x - f' x + (g'' x - g' x)) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf''max:f x f'' xhg''max:g x g'' xf'' x Max.max (f' x) (g' x) + (f'' x - f' x + (g'' x - g' x))I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf''max:f x f'' xhg''max:g x g'' xg'' x Max.max (f' x) (g' x) + (f'' x - f' x + (g'' x - g' x)) All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ithis:MinorizesOn (f'' g'') (f' g' + h) Ihf'g'_integ:IntegrableOn (f' g') I integ (f' g') I = hf'g'_const.integ'upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ithis:MinorizesOn (f'' g'') (f' g' + h) Ihf'g'_integ:IntegrableOn (f' g') I integ (f' g') I = hf'g'_const.integ'hf''g''_integ:IntegrableOn (f'' g'') I integ (f'' g'') I = hf''g''_const.integ'upper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ithis:MinorizesOn (f'' g'') (f' g' + h) Ihf'g'_integ:IntegrableOn (f' g') I integ (f' g') I = hf'g'_const.integ'hf''g''_integ:IntegrableOn (f'' g'') I integ (f'' g'') I = hf''g''_const.integ'hf'g'h_integ:IntegrableOn (f' g' + (f'' - f' + (g'' - g'))) I integ (f' g' + (f'' - f' + (g'' - g'))) I = integ (f' g') I + integ (f'' - f' + (g'' - g')) Iupper_integral (f g) I - lower_integral (f g) I 4 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''max:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εg'': hg''max:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εh: := f'' - f' + (g'' - g')hf'_integ:IntegrableOn f' I integ f' I = hf'const.integ'hg'_integ:IntegrableOn g' I integ g' I = hg'const.integ'hf''_integ:IntegrableOn f'' I integ f'' I = hf''const.integ'hg''_integ:IntegrableOn g'' I integ g'' I = hg''const.integ'hf''f'_integ:IntegrableOn (f'' - f') I integ (f'' - f') I = integ f'' I - integ f' Ihg''g'_integ:IntegrableOn (g'' - g') I integ (g'' - g') I = integ g'' I - integ g' Ihh_IntegrableOn.eq:IntegrableOn (f'' - f' + (g'' - g')) I integ (f'' - f' + (g'' - g')) I = integ (f'' - f') I + integ (g'' - g') Ihinteg_le:integ h I 4 * εhf''g''_const:PiecewiseConstantOn (f'' g'') Ihf''g''_maj:MajorizesOn (f'' g'') (f g) Ihf'g'_const:PiecewiseConstantOn (f' g') Ihf'g'_maj:MinorizesOn (f' g') (f g) Ihff'g''_ge:upper_integral (f g) I hf''g''_const.integ'hf'g'_le:hf'g'_const.integ' lower_integral (f g) Ithis:MajorizesOn (f' g' + h) (f'' g'') Ihf'g'_integ:IntegrableOn (f' g') I integ (f' g') I = hf'g'_const.integ'hf''g''_integ:IntegrableOn (f'' g'') I integ (f'' g'') I = hf''g''_const.integ'hf'g'h_integ:IntegrableOn (f' g' + (f'' - f' + (g'' - g'))) I integ (f' g' + (f'' - f' + (g'' - g'))) I = integ (f' g') I + integ (f'' - f' + (g'' - g')) Iupper_integral (f g) I - lower_integral (f g) I 4 * ε All goals completed! 🐙 exact hmax_bound, I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihmax_bound:BddOn (f g) Ilower_le_upper:0 upper_integral (f g) I - lower_integral (f g) Ithis: (ε : ), 0 < ε upper_integral (f g) I - lower_integral (f g) I 4 * εlower_integral (f g) I = upper_integral (f g) I All goals completed! 🐙

Theorem 11.4.5 / Exercise 11.4.3. The objective here is to create a shorter proof than the one above.

theorem declaration uses `sorry`IntegrableOn.min {I: BoundedInterval} {f g: } (hf: IntegrableOn f I) (hg: IntegrableOn g I) : IntegrableOn (f g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f g) I All goals completed! 🐙

Corollary 11.4.4

theorem IntegrableOn.abs {I: BoundedInterval} {f: } (hf: IntegrableOn f I) : IntegrableOn (abs f) I := I:BoundedIntervalf: hf:IntegrableOn f IIntegrableOn |f| I I:BoundedIntervalf: hf:IntegrableOn f Ithis:IntegrableOn (fun x 0) IIntegrableOn |f| I I:BoundedIntervalf: hf:IntegrableOn f Ithis:IntegrableOn (fun x 0) I|f| = (f fun x 0) - f fun x 0 I:BoundedIntervalf: hf:IntegrableOn f Ithis:IntegrableOn (fun x 0) Ix:|f| x = ((f fun x 0) - f fun x 0) x; obtain h | h := (show f x 0 f x 0 I:BoundedIntervalf: hf:IntegrableOn f IIntegrableOn |f| I All goals completed! 🐙) I:BoundedIntervalf: hf:IntegrableOn f Ithis:IntegrableOn (fun x 0) Ix:h:f x 0|f| x = ((f fun x 0) - f fun x 0) xI:BoundedIntervalf: hf:IntegrableOn f Ithis:IntegrableOn (fun x 0) Ix:h:f x 0|f| x = ((f fun x 0) - f fun x 0) x All goals completed! 🐙

Theorem 11.4.5 (Products preserve Riemann integrability). It is convenient to first establish the non-negative case.

theorem integ_of_mul_nonneg {I: BoundedInterval} {f g: } (hf: IntegrableOn f I) (hg: IntegrableOn g I) (hf_nonneg: MajorizesOn f 0 I) (hg_nonneg: MajorizesOn g 0 I) : IntegrableOn (f * g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I -- This proof is written to follow the structure of the original text. I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyIntegrableOn (f * g) II:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:¬(↑I).NonemptyIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:¬(↑I).NonemptyIntegrableOn (f * g) II:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:¬(↑I).NonemptyIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:¬(↑I).NonemptyI.length = 0 I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:¬(↑I).NonemptySubsingleton I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁IntegrableOn (f * g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂IntegrableOn (f * g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁IntegrableOn (f * g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂IntegrableOn (f * g) I have hmul_bound : BddOn (f * g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂ x I, |(f * g) x| M₁ * M₂; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂x:hx:x IhM₁:|f x| M₁|(f * g) x| M₁ * M₂; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₁pos:0 M₁hM₂pos:0 M₂x:hx:x IhM₁:|f x| M₁hM₂:|g x| M₂|(f * g) x| M₁ * M₂ I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₁pos:0 M₁hM₂pos:0 M₂x:hx:x IhM₁:|f x| M₁hM₂:|g x| M₂|f x| * |g x| M₁ * M₂; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₁pos:0 M₁hM₂pos:0 M₂x:hx:x IhM₁:|f x| M₁hM₂:|g x| M₂0 |g x|I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₁pos:0 M₁hM₂pos:0 M₂x:hx:x IhM₁:|f x| M₁hM₂:|g x| M₂0 M₁ I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₁pos:0 M₁hM₂pos:0 M₂x:hx:x IhM₁:|f x| M₁hM₂:|g x| M₂0 |g x|I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₁pos:0 M₁hM₂pos:0 M₂x:hx:x IhM₁:|f x| M₁hM₂:|g x| M₂0 M₁ All goals completed! 🐙 have lower_le_upper : 0 upper_integral (f * g) I - lower_integral (f * g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I All goals completed! 🐙 have (ε:) (: 0 < ε) : upper_integral (f * g) I - lower_integral (f * g) I 2*(M₁+M₂)*ε := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I have : f', MinorizesOn f' f I PiecewiseConstantOn f' I integ f I - ε < PiecewiseConstantOn.integ f' I MajorizesOn f' 0 I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I choose f' hf'min hf'const hf'int using gt_of_lt_lower_integral hf.1 (show integ f I - ε < lower_integral f I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I All goals completed! 🐙) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' IMinorizesOn (f' 0) f I PiecewiseConstantOn (f' 0) I integ f I - ε < PiecewiseConstantOn.integ (f' 0) I MajorizesOn (f' 0) 0 I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) IMinorizesOn (f' 0) f I PiecewiseConstantOn (f' 0) I integ f I - ε < PiecewiseConstantOn.integ (f' 0) I MajorizesOn (f' 0) 0 I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) IMinorizesOn (f' 0) f II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) IPiecewiseConstantOn (f' 0) II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) Iinteg f I - ε < PiecewiseConstantOn.integ (f' 0) II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) IMajorizesOn (f' 0) 0 I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) IMinorizesOn (f' 0) f I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) Ix:hx:x Ithis:0 x f x(f' 0) x f x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) Ix:hx:x Ithis:0 x f xhf'min:f' x f x(f' 0) x f x; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) IPiecewiseConstantOn (f' 0) I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) Iinteg f I - ε < PiecewiseConstantOn.integ (f' 0) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) I x I, f' x (f' fun x 0) x; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihzero:PiecewiseConstantOn (fun x 0) Ix✝:x✝ I 0 x✝ (f' 0) x✝; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε have : g', MinorizesOn g' g I PiecewiseConstantOn g' I integ g I - ε < PiecewiseConstantOn.integ g' I MajorizesOn g' 0 I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I obtain g', hg'min, hg'const, hg'int := gt_of_lt_lower_integral hg.1 (show integ g I - ε < lower_integral g I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I All goals completed! 🐙) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' IMinorizesOn (g' 0) g I PiecewiseConstantOn (g' 0) I integ g I - ε < PiecewiseConstantOn.integ (g' 0) I MajorizesOn (g' 0) 0 I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) IMinorizesOn (g' 0) g I PiecewiseConstantOn (g' 0) I integ g I - ε < PiecewiseConstantOn.integ (g' 0) I MajorizesOn (g' 0) 0 I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) IMinorizesOn (g' 0) g II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) IPiecewiseConstantOn (g' 0) II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) Iinteg g I - ε < PiecewiseConstantOn.integ (g' 0) II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) IMajorizesOn (g' 0) 0 I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) IMinorizesOn (g' 0) g I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) Ix:hx:x Ithis:0 x g x(g' 0) x g x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) Ix:hx:x Ithis:0 x g xhg'min:g' x g x(g' 0) x g x; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) IPiecewiseConstantOn (g' 0) I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) Iinteg g I - ε < PiecewiseConstantOn.integ (g' 0) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) I x I, g' x (g' fun x 0) x; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihzero:PiecewiseConstantOn (fun x 0) Ix✝:x✝ I 0 x✝ (g' 0) x✝; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε have : f'', MajorizesOn f'' f I PiecewiseConstantOn f'' I PiecewiseConstantOn.integ f'' I < integ f I + ε MinorizesOn f'' (fun _ M₁) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I obtain f'', hf''maj, hf''const, hf''int := lt_of_gt_upper_integral hf.1 (show upper_integral f I < integ f I + ε I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I All goals completed! 🐙) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εMajorizesOn (f'' fun x M₁) f I PiecewiseConstantOn (f'' fun x M₁) I PiecewiseConstantOn.integ (f'' fun x M₁) I < integ f I + ε MinorizesOn (f'' fun x M₁) (fun x M₁) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IMajorizesOn (f'' fun x M₁) f I PiecewiseConstantOn (f'' fun x M₁) I PiecewiseConstantOn.integ (f'' fun x M₁) I < integ f I + ε MinorizesOn (f'' fun x M₁) (fun x M₁) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IMajorizesOn (f'' fun x M₁) f II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IPiecewiseConstantOn (f'' fun x M₁) II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IPiecewiseConstantOn.integ (f'' fun x M₁) I < integ f I + εI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IMinorizesOn (f'' fun x M₁) (fun x M₁) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IMajorizesOn (f'' fun x M₁) f I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) Ix:hx:x IhM₁:|f x| M₁f x (f'' fun x M₁) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁✝: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) Ix:hx:x IhM₁:f x M₁ -f x M₁f x (f'' fun x M₁) x All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IPiecewiseConstantOn (f'' fun x M₁) I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) IPiecewiseConstantOn.integ (f'' fun x M₁) I < integ f I + ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) I x I, (f'' fun x M₁) x f'' x All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhM₁_piece:PiecewiseConstantOn (fun x M₁) Ix✝:x✝ I (f'' fun x M₁) x✝ (fun x M₁) x✝; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε have : g'', MajorizesOn g'' g I PiecewiseConstantOn g'' I PiecewiseConstantOn.integ g'' I < integ g I + ε MinorizesOn g'' (fun _ M₂) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I obtain g'', hg''maj, hg''const, hg''int := lt_of_gt_upper_integral hg.1 (show upper_integral g I < integ g I + ε I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I All goals completed! 🐙) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εMajorizesOn (g'' fun x M₂) g I PiecewiseConstantOn (g'' fun x M₂) I PiecewiseConstantOn.integ (g'' fun x M₂) I < integ g I + ε MinorizesOn (g'' fun x M₂) (fun x M₂) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IMajorizesOn (g'' fun x M₂) g I PiecewiseConstantOn (g'' fun x M₂) I PiecewiseConstantOn.integ (g'' fun x M₂) I < integ g I + ε MinorizesOn (g'' fun x M₂) (fun x M₂) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IMajorizesOn (g'' fun x M₂) g II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IPiecewiseConstantOn (g'' fun x M₂) II:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IPiecewiseConstantOn.integ (g'' fun x M₂) I < integ g I + εI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IMinorizesOn (g'' fun x M₂) (fun x M₂) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IMajorizesOn (g'' fun x M₂) g I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂✝: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) Ix:hx:x IhM₂:|g x| M₂g x (g'' fun x M₂) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂✝: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) Ix:hx:x IhM₂:g x M₂ -g x M₂g x (g'' fun x M₂) x All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IPiecewiseConstantOn (g'' fun x M₂) I All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) IPiecewiseConstantOn.integ (g'' fun x M₂) I < integ g I + ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) I x I, (g'' fun x M₂) x g'' x All goals completed! 🐙 intro _ I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhM₂_piece:PiecewiseConstantOn (fun x M₂) Ix✝:a✝:x✝ I(g'' fun x M₂) x✝ (fun x M₂) x✝; All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε have hf'g'_maj : MinorizesOn (f' * g') (f * g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f x(f' * g') x (f * g) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g x(f' * g') x (f * g) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf'_nonneg:0 x f' x(f' * g') x (f * g) x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf'_nonneg:0 x f' xhg'_nonneg:0 x g' x(f' * g') x (f * g) x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf'_nonneg:0 f' xhg'_nonneg:0 g' xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) If' x * g' x f x * g x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf'_nonneg:0 f' xhg'_nonneg:0 g' xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 g' xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf'_nonneg:0 f' xhg'_nonneg:0 g' xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 f x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf'_nonneg:0 f' xhg'_nonneg:0 g' xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 g' xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min✝:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ig': hg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ix:hx:x Ihf'min:f' x f xhg'min:g' x g xhf'_nonneg:0 f' xhg'_nonneg:0 g' xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 f x All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε have hf''g''_maj : MajorizesOn (f'' * g'') (f * g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' x(f * g) x (f'' * g'') x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' x(f * g) x (f'' * g'') x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' xhg_nonneg:0 x g x(f * g) x (f'' * g'') x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' xhg_nonneg:0 x g xhf_nonneg:0 x f x(f * g) x (f'' * g'') x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' xhg_nonneg:0 g xhf_nonneg:0 f xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) If x * g x f'' x * g'' x; I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' xhg_nonneg:0 g xhf_nonneg:0 f xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 g xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' xhg_nonneg:0 g xhf_nonneg:0 f xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 f'' x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' xhg_nonneg:0 g xhf_nonneg:0 f xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 g xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj✝:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ix:hx:x Ihf''maj:f x f'' xhg''maj:g x g'' xhg_nonneg:0 g xhf_nonneg:0 f xlower_le_upper:lower_integral (f * g) I upper_integral (f * g) I0 f'' x All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'upper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε have hhmin : MinorizesOn (f'' * g'' - f' * g') (M₁ (g''-g') + M₂ (f''-f')) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IIntegrableOn (f * g) I intro x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x I(f'' * g'' - f' * g') x (M₁ (g'' - g') + M₂ (f'' - f')) x I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x If'' x * g'' x - f' x * g' x M₁ * (g'' x - g' x) + M₂ * (f'' x - f' x) calc _ = (f'' x) * (g'' x - g' x) + (g' x) * (f'' x - f' x) := I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x If'' x * g'' x - f' x * g' x = f'' x * (g'' x - g' x) + g' x * (f'' x - f' x) All goals completed! 🐙 _ _ := I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x If'' x * (g'' x - g' x) + g' x * (f'' x - f' x) M₁ * (g'' x - g' x) + M₂ * (f'' x - f' x) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x I0 g'' x - g' xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x If'' x M₁I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x I0 f'' x - f' xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x Ig' x M₂ I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x I0 g'' x - g' xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x If'' x M₁I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x I0 f'' x - f' xI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ix:hx:x Ig' x M₂ All goals completed! 🐙 I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) Iupper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * ε calc _ M₁ * PiecewiseConstantOn.integ (g'' - g') I + M₂ * PiecewiseConstantOn.integ (f'' - f') I := I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) Iupper_integral (f * g) I - lower_integral (f * g) I M₁ * PiecewiseConstantOn.integ (g'' - g') I + M₂ * PiecewiseConstantOn.integ (f'' - f') I All goals completed! 🐙 _ M₁ * (2*ε) + M₂ * (2*ε) := I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) IM₁ * PiecewiseConstantOn.integ (g'' - g') I + M₂ * PiecewiseConstantOn.integ (f'' - f') I M₁ * (2 * ε) + M₂ * (2 * ε) I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) IPiecewiseConstantOn.integ (g'' - g') I 2 * εI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) IPiecewiseConstantOn.integ (f'' - f') I 2 * ε I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) IPiecewiseConstantOn.integ (g'' - g') I 2 * εI:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) IPiecewiseConstantOn.integ (f'' - f') I 2 * ε All goals completed! 🐙 _ = _ := I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Iε::0 < εf': hf'min:MinorizesOn f' f Ihf'const:PiecewiseConstantOn f' Ihf'int:integ f I - ε < PiecewiseConstantOn.integ f' Ihf'_nonneg:MajorizesOn f' 0 Ig': hg'min:MinorizesOn g' g Ihg'const:PiecewiseConstantOn g' Ihg'int:integ g I - ε < PiecewiseConstantOn.integ g' Ihg'_nonneg:MajorizesOn g' 0 If'': hf''maj:MajorizesOn f'' f Ihf''const:PiecewiseConstantOn f'' Ihf''int:PiecewiseConstantOn.integ f'' I < integ f I + εhf''bound:MinorizesOn f'' (fun x M₁) Ig'': hg''maj:MajorizesOn g'' g Ihg''const:PiecewiseConstantOn g'' Ihg''int:PiecewiseConstantOn.integ g'' I < integ g I + εhg''bound:MinorizesOn g'' (fun x M₂) Ihf'g'_const:PiecewiseConstantOn (f' * g') Ihf'g'_maj:MinorizesOn (f' * g') (f * g) Ihf''g''_const:PiecewiseConstantOn (f'' * g'') Ihf''g''_maj:MajorizesOn (f'' * g'') (f * g) Ihupper_le:upper_integral (f * g) I hf''g''_const.integ'hlower_ge:hf'g'_const.integ' lower_integral (f * g) Ihh_const:PiecewiseConstantOn (f'' * g'' - f' * g') Ihh_integ:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I = PiecewiseConstantOn.integ (f'' * g'') I - PiecewiseConstantOn.integ (f' * g') Ihhmin:MinorizesOn (f'' * g'' - f' * g') (M₁ (g'' - g') + M₂ (f'' - f')) Ihg''g'_const:PiecewiseConstantOn (g'' - g') Ihg''g'_integ:PiecewiseConstantOn.integ (g'' - g') I = PiecewiseConstantOn.integ g'' I - PiecewiseConstantOn.integ g' IhM₁g''g'_const:PiecewiseConstantOn (M₁ (g'' - g')) IhM₁g''g_integ:PiecewiseConstantOn.integ (M₁ (g'' - g')) I = M₁ * PiecewiseConstantOn.integ (g'' - g') Ihf''f'_const:PiecewiseConstantOn (f'' - f') Ihf''f_integ:PiecewiseConstantOn.integ (f'' - f') I = PiecewiseConstantOn.integ f'' I - PiecewiseConstantOn.integ f' IhM₂f''f'_const:PiecewiseConstantOn (M₂ (f'' - f')) IhM₂f''f_integ:PiecewiseConstantOn.integ (M₂ (f'' - f')) I = M₂ * PiecewiseConstantOn.integ (f'' - f') Ihsum_const:PiecewiseConstantOn (M₁ (g'' - g') + M₂ (f'' - f')) Ihsum_integ:PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) I = PiecewiseConstantOn.integ (M₁ (g'' - g')) I + PiecewiseConstantOn.integ (M₂ (f'' - f')) Ihsum_bound:PiecewiseConstantOn.integ (f'' * g'' - f' * g') I PiecewiseConstantOn.integ (M₁ (g'' - g') + M₂ (f'' - f')) IM₁ * (2 * ε) + M₂ * (2 * ε) = 2 * (M₁ + M₂) * ε All goals completed! 🐙 exact hmul_bound, I:BoundedIntervalf: g: hf:BddOn f I lower_integral f I = upper_integral f Ihg:BddOn g I lower_integral g I = upper_integral g Ihf_nonneg:MajorizesOn f 0 Ihg_nonneg:MajorizesOn g 0 IhI:(↑I).NonemptyM₁:hM₁: x I, |f x| M₁M₂:hM₂: x I, |g x| M₂hM₁pos:0 M₁hM₂pos:0 M₂hmul_bound:BddOn (f * g) Ilower_le_upper:0 upper_integral (f * g) I - lower_integral (f * g) Ithis: (ε : ), 0 < ε upper_integral (f * g) I - lower_integral (f * g) I 2 * (M₁ + M₂) * εlower_integral (f * g) I = upper_integral (f * g) I All goals completed! 🐙
theorem integ_of_mul {I: BoundedInterval} {f g: } (hf: IntegrableOn f I) (hg: IntegrableOn g I) : IntegrableOn (f * g) I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f * g) I -- This proof is written to follow the structure of the original text. I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0IntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)IntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0IntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)IntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus IIntegrableOn (f * g) I have hfplus_nonneg : MajorizesOn fplus 0 I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ix✝:x✝ I 0 x✝ fplus x✝; All goals completed! 🐙 have hfminus_nonneg : MajorizesOn fminus 0 I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ix✝:x✝ I 0 x✝ fminus x✝; All goals completed! 🐙 have hgplus_nonneg : MajorizesOn gplus 0 I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ix✝:x✝ I 0 x✝ gplus x✝; All goals completed! 🐙 have hgminus_nonneg : MajorizesOn gminus 0 I := I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ihgplus_nonneg:MajorizesOn gplus 0 Ix✝:x✝ I 0 x✝ gminus x✝; All goals completed! 🐙 I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ihgplus_nonneg:MajorizesOn gplus 0 Ihgminus_nonneg:MajorizesOn gminus 0 Ihfplusgplus:IntegrableOn ((f fun x 0) * (g fun x 0)) IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ihgplus_nonneg:MajorizesOn gplus 0 Ihgminus_nonneg:MajorizesOn gminus 0 Ihfplusgplus:IntegrableOn ((f fun x 0) * (g fun x 0)) Ihfplusgminus:IntegrableOn ((f fun x 0) * gminus) IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ihgplus_nonneg:MajorizesOn gplus 0 Ihgminus_nonneg:MajorizesOn gminus 0 Ihfplusgplus:IntegrableOn ((f fun x 0) * (g fun x 0)) Ihfplusgminus:IntegrableOn ((f fun x 0) * gminus) Ihfminusgplus:IntegrableOn (fminus * (g fun x 0)) IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ihgplus_nonneg:MajorizesOn gplus 0 Ihgminus_nonneg:MajorizesOn gminus 0 Ihfplusgplus:IntegrableOn ((f fun x 0) * (g fun x 0)) Ihfplusgminus:IntegrableOn ((f fun x 0) * gminus) Ihfminusgplus:IntegrableOn (fminus * (g fun x 0)) Ihfminusgminus:IntegrableOn (fminus * gminus) IIntegrableOn (f * g) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ihgplus_nonneg:MajorizesOn gplus 0 Ihgminus_nonneg:MajorizesOn gminus 0 Ihfplusgplus:IntegrableOn ((f fun x 0) * (g fun x 0)) Ihfplusgminus:IntegrableOn ((f fun x 0) * gminus) Ihfminusgplus:IntegrableOn (fminus * (g fun x 0)) Ihfminusgminus:IntegrableOn (fminus * gminus) IIntegrableOn ((fplus - fminus) * (gplus - gminus)) I I:BoundedIntervalf: g: hf:IntegrableOn f Ihg:IntegrableOn g Ifplus: := f fun x 0fminus: := -(f fun x 0)gplus: := g fun x 0gminus: := -(g fun x 0)this:IntegrableOn (fun x 0) Ihfplus_integ:IntegrableOn (f fun x 0) Ihgplus_integ:IntegrableOn (g fun x 0) Ihfminus_integ:IntegrableOn fminus Ihgminus_integ:IntegrableOn gminus Ihfplus_nonneg:MajorizesOn fplus 0 Ihfminus_nonneg:MajorizesOn fminus 0 Ihgplus_nonneg:MajorizesOn gplus 0 Ihgminus_nonneg:MajorizesOn gminus 0 Ihfplusgplus:IntegrableOn ((f fun x 0) * (g fun x 0)) Ihfplusgminus:IntegrableOn ((f fun x 0) * gminus) Ihfminusgplus:IntegrableOn (fminus * (g fun x 0)) Ihfminusgminus:IntegrableOn (fminus * gminus) IIntegrableOn (fplus * gplus + (-(fplus * gminus) - fminus * gplus) + fminus * gminus) I All goals completed! 🐙open BoundedInterval

Exercise 11.4.2

theorem declaration uses `sorry`IntegrableOn.split {I: BoundedInterval} {f: } (hf: IntegrableOn f I) (P: Partition I) : integ f I = J P.intervals, integ f J := I:BoundedIntervalf: hf:IntegrableOn f IP:Partition Iinteg f I = J P.intervals, integ f J All goals completed! 🐙
end Chapter11