:: On the Properties of Curves and Parametrization-Independent Isoperimetric Inequality
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received December 14, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

LmPI: 0 < PI
by LEIBNIZ1:17;

definition

let a, b be Real;
let x, y be PartFunc of REAL,REAL;

func ArcLenP (x,y,a,b) -> PartFunc of REAL,REAL means :Def1: :: CURVE:def 1
( dom it = [.a,b.] & ( for t being Real st t in [.a,b.] holds
it . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) );

existence
ex b₁ being PartFunc of REAL,REAL st
( dom b₁ = [.a,b.] & ( for t being Real st t in [.a,b.] holds
b₁ . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of REAL,REAL st dom b₁ = [.a,b.] & ( for t being Real st t in [.a,b.] holds
b₁ . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) & dom b₂ = [.a,b.] & ( for t being Real st t in [.a,b.] holds
b₂ . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines ArcLenP CURVE:def 1 :
for a, b being Real
for x, y, b₅ being PartFunc of REAL,REAL holds
( b₅ = ArcLenP (x,y,a,b) iff ( dom b₅ = [.a,b.] & ( for t being Real st t in [.a,b.] holds
b₅ . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) ) );

Lm1: for a, b being Real holds ].a,b.[ c= [.a,b.]
by XXREAL_1:25;

theorem Th1: :: CURVE:1

for a, b, d being Real
for f being PartFunc of REAL,REAL st a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous & f . a < d & d < f . b holds
ex c being Real st
( a < c & c < b & d = f . c )

proof end;

theorem Th2: :: CURVE:2

for a, b being Real
for Z being open Subset of REAL st a < b & [.a,b.] c= Z holds
ex a1, b1 being Real st
( a1 < a & b < b1 & a1 < b1 & [.a1,b1.] c= Z & [.a,b.] c= ].a1,b1.[ )

proof end;

theorem Th3: :: CURVE:3

for a, b being Real
for x, y being PartFunc of REAL,REAL st a < b & x is differentiable & y is differentiable & [.a,b.] c= dom x & [.a,b.] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
0 < ((diff (x,t)) ^2) + ((diff (y,t)) ^2) ) holds
ex a1, b1 being Real ex l being PartFunc of REAL,REAL ex Z being open Subset of REAL st
( a1 < a & b < b1 & Z = (dom x) /\ (dom y) & [.a,b.] c= ].a1,b1.[ & [.a1,b1.] c= Z & dom l = Z & ( for t being Real st t in [.a1,b1.] holds
l . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a1,t) ) & l is_differentiable_on ].a1,b1.[ & l `| ].a1,b1.[ = ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ].a1,b1.[ & l `| ].a1,b1.[ is continuous & ( for t being Real st t in ].a1,b1.[ holds
( l is_differentiable_in t & diff (l,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) ) ) & ( for t being Real st t in [.a,b.] holds
(ArcLenP (x,y,a,b)) . t = (l . t) - (l . a) ) )

proof end;

theorem Th4: :: CURVE:4

for a, b being Real
for x, y being PartFunc of REAL,REAL st a < b & x is differentiable & y is differentiable & [.a,b.] c= dom x & [.a,b.] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
0 < ((diff (x,t)) ^2) + ((diff (y,t)) ^2) ) holds
ex a1, b1 being Real ex L being one-to-one PartFunc of REAL,REAL st
( a1 < a & b < b1 & [.a1,b1.] c= (dom x) /\ (dom y) & dom L = ].a1,b1.[ & ( for t being Real st t in ].a1,b1.[ holds
L . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a1,t) ) & ( for t being Real st t in [.a,b.] holds
(ArcLenP (x,y,a,b)) . t = (L . t) - (L . a) ) & L is increasing & L | [.a,b.] is continuous & L .: [.a,b.] = [.(L . a),(L . b).] & ( for t being Real st t in ].a1,b1.[ holds
L is_differentiable_in t ) & L is_differentiable_on ].a1,b1.[ & ( for t being Real st t in ].a1,b1.[ holds
diff (L,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) ) & L " is_differentiable_on dom (L ") & ( for t being Real st t in dom (L ") holds
diff ((L "),t) = 1 / (diff (L,((L ") . t))) ) & L " is continuous & ( for s being Real st s in rng L holds
( x * (L ") is_differentiable_in s & y * (L ") is_differentiable_in s & diff ((x * (L ")),s) = (diff (x,((L ") . s))) * (diff ((L "),s)) & diff ((y * (L ")),s) = (diff (y,((L ") . s))) * (diff ((L "),s)) & ((diff ((x * (L ")),s)) ^2) + ((diff ((y * (L ")),s)) ^2) = 1 ) ) & (x * (L ")) `| (dom (x * (L "))) = ((x `| (dom x)) * (L ")) (#) ((L ") `| (dom (L "))) & (y * (L ")) `| (dom (y * (L "))) = ((y `| (dom y)) * (L ")) (#) ((L ") `| (dom (L "))) & (L ") `| (dom (L ")) = ((L `| (dom L)) * (L ")) ^ & (L ") `| (dom (L ")) is continuous & [.(L . a),(L . b).] c= dom (L ") & [.(L . a),(L . b).] c= dom (x * (L ")) & [.(L . a),(L . b).] c= dom (y * (L ")) & [.(L . a),(L . b).] c= rng L & dom (x * (L ")) = dom (L ") & dom (y * (L ")) = dom (L ") & x * (L ") is differentiable & y * (L ") is differentiable & (x * (L ")) `| (dom (x * (L "))) is continuous & (y * (L ")) `| (dom (y * (L "))) is continuous & ( for s being Real st s in (dom (x * (L "))) /\ (dom (y * (L "))) holds
((diff ((x * (L ")),s)) ^2) + ((diff ((y * (L ")),s)) ^2) = 1 ) & integral ((y (#) (x `| (dom x))),a,b) = integral (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))),(L . a),(L . b)) )

proof end;

Lm2: for f being PartFunc of REAL,REAL
for N being open Subset of REAL st dom f = REAL & f is continuous holds
f " N is open

proof end;

Lm3: for x, y being PartFunc of REAL,REAL
for a, b being Real st a < b & x is differentiable & y is differentiable & ['a,b'] c= dom x & ['a,b'] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = 1 ) & y . a = 0 & y . b = 0 holds
( integral ((y (#) (x `| (dom x))),a,b) <= ((1 / 2) * ((b - a) ^2)) / PI & ( not integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * ((b - a) ^2)) / PI or for t being Real st t in [.a,b.] holds
( y . t = ((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a))) & x . t = ((b - a) / PI) * (((- (cos . ((PI * (t - a)) / (b - a)))) + (cos . 0)) + ((PI / (b - a)) * (x . a))) ) or for t being Real st t in [.a,b.] holds
( y . t = - (((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a)))) & x . t = ((b - a) / PI) * (((cos . ((PI * (t - a)) / (b - a))) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ) & ( ( for t being Real st t in [.a,b.] holds
( y . t = ((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a))) & x . t = ((b - a) / PI) * (((- (cos . ((PI * (t - a)) / (b - a)))) + (cos . 0)) + ((PI / (b - a)) * (x . a))) ) or for t being Real st t in [.a,b.] holds
( y . t = - (((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a)))) & x . t = ((b - a) / PI) * (((cos . ((PI * (t - a)) / (b - a))) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ) implies integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * ((b - a) ^2)) / PI ) )

proof end;

theorem :: CURVE:5

for a, b, l being Real
for x, y being PartFunc of REAL,REAL st a < b & (ArcLenP (x,y,a,b)) . b = l & y . a = 0 & y . b = 0 & x is differentiable & y is differentiable & [.a,b.] c= dom x & [.a,b.] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
0 < ((diff (x,t)) ^2) + ((diff (y,t)) ^2) ) holds
( integral ((y (#) (x `| (dom x))),a,b) <= ((1 / 2) * (l ^2)) / PI & ( not integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * (l ^2)) / PI or for s being Real st s in [.a,b.] holds
( y . s = (l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) & x . s = (l / PI) * (((- (cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) + (cos . 0)) + ((PI / l) * (x . a))) ) or for s being Real st s in [.a,b.] holds
( y . s = - ((l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) & x . s = (l / PI) * (((cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) - (cos . 0)) + ((PI / l) * (x . a))) ) ) & ( ( for s being Real st s in [.a,b.] holds
( y . s = (l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) & x . s = (l / PI) * (((- (cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) + (cos . 0)) + ((PI / l) * (x . a))) ) or for s being Real st s in [.a,b.] holds
( y . s = - ((l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) & x . s = (l / PI) * (((cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) - (cos . 0)) + ((PI / l) * (x . a))) ) ) implies integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * (l ^2)) / PI ) )

proof end;